For all casual users of subversion: if you don't want to set the
"svn:keywords" property by hand all the time, you may consider to merge
the following into your ~/.subversion/config:
[miscellany]
enable-auto-props = yes
[auto-props]
*.ML = svn:keywords=Id
*.hs = svn:keywords=Id
*.thy = svn:keywor
A)
"code_gen" command now takes optional "to" part; if given, *all*
generated code is packaged into the same structure / module / name
space, with name given after "to":
code_gen in to file
Syntax is still open for discussion.
B)
Code generation for SML no longer generates outermost "ROOT"
Syntactic class Orderings.ord moved to HOL (to faciliate HOL-Main
bootstrap).
Consequently, constant Orderings.ord_class.less(_eq) now named
HOL.ord_class.less(_eq). For direct references to these constant names
in ML code snippets, code antiquotation expressions @{const_name
HOL.less_eq} and @{co
"Sup" is now a parameter for class complete_lattice rather than a
derived definition. INCOMPATIBILITY. Instantation of class
complete_lattice requires explicit definition for "Sup". Corresponding
theorem renames:
Sup_def ~> Sup_Inf
Sup_bool_eq ~> Sup_bool_def
Sup_set_eq ~> Sup_set_d
Theory Finite_Set: "name-space" locales Lattice, Distrib_lattice,
Linorder etc. have disappeared; operations defined in terms of fold_set
now are named Inf_fin, Sup_fin. INCOMPATIBILITY.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: signature
Keyword "code_gen" now named "export_code".
Florian
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 249 bytes
Desc: OpenPGP digital signature
Url :
https://mailmanbroy.informatik.tu-muenchen.de/piperm
(1) I discovered a slip in the implementation of Rat.inv which did not
normalize negative rats; this might explain the strange behaviour of
equality (fixed in CVS).
(2) I strongly support Amine's issue: all code generator frameworks
should use the verified rational numbers. Why I have refrained s
> Florian has suggested making sledgehammer available earlier in the
> construction of Main, before PreList at least. This could be useful
> to developers. However, it requires Hilbert_Choice, which must also
> be introduced earlier.
A PreList-Sledgehammer would be a nice thing to have, but
Lawrence Paulson wrote:
> It needs at least Hilbert_Choice. It could go before Datatype. Some
> details need to be worked out to ensure that all theorems in Main.thy
> get converted to clause form.
I must confess that I have lost track now. Does only the skolemization
depend on Hilbert-Choice, or
Lawrence Paulson wrote:
> Metis also relies on clause form.
I would still argue that it is a good idea to have a non-Hilbertian
entrance point to HOL (PreList); anyway there should be no problem to
import Hilbert_Choice before List and then setup Metis and Sledgehammer.
Florian
-- ne
ATP prover default locations are now platform-sensitive; use
isatool getenv ML_PLATFORM
to inspect your platform identifier. Then default locations are
$ISABELLE_HOME/contrib/E/$ML_PLATFORM/
$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM/
$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/b
in.tum.de
CC: minamide at cs.tsukuba.ac.jp
Dear Florian Haftmann,
I would like to report you a small problem I encoutered during my
development. (Since it is a small problem, I hesitate to post it
to the isabelle mailing list.)
I encounter the following problem in print translation
when a polymorphic
Specifications in class declarations now allow for canonical local
syntax. In particular, additional local syntax declarations and local
derived constants may be referred to directly.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type:
Consolidated naming conventions in some code-generator-specific library
theories:
* Pretty_Int ~> Code_Integer
* Pretty_Char ~> Code_Char
* Pretty_Char_ord ~> Code_Char_ord
* ML_Int ~> Code_Index, ml_int ~> index
* ML_String ~> Code_Message, ml_string ~> message_string
-- next
Class-context aware syntax for class target ("user space type system"):
Local operations in class context (fixes, definitions, axiomatizations,
abbreviations) are identified with their global counterparts during
reading and printing of terms. Practically, this allows to use the same
syntax for bo
Normalization by evaluation now considers type classes via explicit
dictionary construction. Available via command ``normal_form'' and
method ``normalization''.
Florian
--
PGP available:
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de.p
>>> The class recpower is very unfortunate. I suggest to remove it and
>>> replace it by definitions inside the locale/class (The axioms *are* a
>>> recursive function definition).
The class is surely an accident; however it has been there for 3 years
now. We still have enough time after the Isab
> Not to mention foo_tac ;-)
>
> The English language has the term blacklist. Isar has a redlist.
I will take this opportunity to propose again a new xsymbol which is
printed as a *red* dot and stands for "using prems ." ;-)
Florian
-- next part --
A non-text atta
* Command "instance" now takes list of definitions in the same manner as
the "definition" command. Most notably, object equality is now
possible. Type inference is more canonical than it used to be.
INCOMPATIBILITY: in some cases explicit type annotations are required.
Florian
-
Amine Chaieb schrieb:
> Zur Antwort auf der Gestern gestellte Frage: was ist die bis jetzt
> groesste Zahl von der wir Primalitaet zeigen koennen:
>
> val it =
> "prime
>
> 2591170860132026277762467679224415309418188875531254273039749231618740192665863620862012095168004834065506952417331941
> I just discovered that another last minute "FIXME" has changed the
> hierarchy of rings in Isabelle2007 such that "real" is not of sort
> "lordered_ring" any more. More generally, "ordered_ring" is not an
> "lordered_ring" any more. This is pretty unfortunate as it renders the
> whole HOL-Com
The maintainer of XEmacs on MacPorts just has informed me that Mule/Sumo
is now the default. I've updated the website accordingly.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not
* New primrec package. Specification syntax conforms in style to
definition/function/ No separate induction rule is provided. The
"primrec" command distinguishes old-style and new-style specifications
by syntax. The former primrec package is now named OldPrimrecPackage.
When adjusting theori
Dear Brian,
there is a problem with some HOLCF updates you have recently checked in.
In theory Pcpo.thy, there is a reference to a class "ppo" which is not
present. Maybe you forgot to do cvs add or something alike!?
Cheers
Florian
-- next part --
A non-text attachment w
Instantiation target allows for simultaneous specification of class
instance operations together with an instantiation proof. Type check
phase allows to refer to class operations uniformly. See
HOL/Complex/Complex.thy for an Isar example and HOL/Library/Eval.thy for
an ML interface example.
> It all comes down to the line
>
> val unit = (fn Const ("Unity",_) => true | _ => false);
>
> in HOL/Tools/record_package.ML which doesn't match Unity correctly.
>
> Unfortunately, replacing it by @{term "Unity} or @[term "()"} doesn't work.
Since this is part of the syntax layer,
Dear Brian,
> Today I modified a copy of Isabelle/HOL in this way; everything seems to
> work just fine, and binary arithmetic works faster. However, code
> generation will need a bit more work, and the HOL/Word library will need
> some non-trivial modifications.
The issue with code generation is
>> val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
>> _ => false);
>
> It's not entirely satisfying (I was hoping I could get away with not
> mentioning Product_Type), but better than what I had before. I'll commit
> this then.
Indeed, the Product_Type is not necess
In latex output, it is now possible to insert the specification of a
datatype:
text {* ... @{datatype list} ... *}
Comments and suggestions welcome.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 6
Dear Michael,
> I want to set up a locale with an Element.Assumes element that gives
> an assumption that I want marked with the "simp" attribute.
>
> In other words, I want to construct something like
>
> Element.Assumes
> [((, [ ??? ]),
> [(, [])])]
>
> where thi
> the next official release is likely to happen this spring, probably at the
> end of May or beginning of June. This means there are still some weeks to
> consolidate existing features, before the usual freezing period of 2-3
> weeks before the actual release date.
This is also a nice opportun
> * Antiquotation "lemma" takes a proposition and a simple method text as
> argument
> and asserts that the proposition is provable by the corresponding method
> invocation. Prints text of proposition, as does antiquotation "prop". A
> simple
> method text is either a method name or a method na
Call me stupid, but I don't see any difference between the following two
function definitions in Pure/thm.ML:
> fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
> let val A = Term.argument_type_of c 0
> in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx,
* Command 'rep_datatype': instead of theorem names the command now
takes a list of terms denoting the constructors of the type to be
represented as datatype. The characteristic theorems have to be
proven. INCOMPATIBILITY. Also observe that the following theorems
have disappeared in favour of exi
Hi Brian,
first of all, I want to emphasize that the merging of HOL-Complex with
HOL is not necessarily the final state. We are still experimenting and
collecting feedback,
> What is the rationale behind merging HOL-Complex with HOL?
> I would guess that the real reason for the merge is that som
what I forgot to mention:
There is no urgent need that the HOL image contains *all* the
HOL-Complex theories. I also have been thinking about splitting off all
the Analysis stuff into a session HOL-Analysis, but on the other hand a
lot of functions which you naively expect for reals/complexes (lo
New ML antiquotation 'code': takes constant as argument, generates
corresponding code in background and inserts name of the corresponding
resulting ML value/function/datatype constructor binding in place. All
occurences of 'code' with a single ML block are generated simultaneously.
Provides a gene
Dear all,
last week I spent some considerable time and energy to get rid of the
locale (open) feature, which was in most cases straight forward and
trivial -- except the issue of MicroJava, Jinja, JinjaThreads. I think
it is worth to document my experiences here for the future.
The three obfusc
Tobias Nipkow wrote:
>> The three obfuscating issues were:
>>
>> A) Archaic, hardly readable and fragile proof techniques:
>> * unfolding definitions of predicates over logical formulae instead of
>> proper intro/elim-rules
>
> This is mere dogma. It is perfectly standard to reason about log
Amine Chaieb wrote:
> I don't see why this argument yields an "iff" proof of your conjecture.
Sometimes a typo is only a typo, nothing more. I don't want to state a
general guideline for that issue, but only report my (subjective)
experiences concerning particular examples.
Florian
-
* Integrated image HOL-Complex with HOL. Entry points Main.thy and
Complex_Main.thy remain as they are.
* New image HOL-Plain provides a minimal HOL with the most important
tools available (inductive, datatype, primrec, ...). By convention the
corresponding theory Plain should be ancestor of eve
The overloaded infix syntax "^" for different power operations (natural
power in monoids, function power, relation power) turns more and more
unsatisfactory for a couple of reasons, e.g.:
* The abuse of the type class mechanism to achieve the "^" syntax for
funpow and relpow hinders the enforcemen
a) On theory merge, the last set of code equations for a particular
constant is taken (in accordance with the policy applied by other
parts of the code generator framework).
b) Code equations stemming from explicit declarations (e.g. code
attribute) gain priority over default code equation
HOL/Main: command "value" now integrates different evaluation
mechanisms. The result of the first successful evaluation mechanism is
printed. In square brackets a particular named evaluation mechanisms
may be specified (currently, [SML], [code] or [nbe] -- suggestions for
better syntax welcome).
Normalization by evaluation now allows non-leftlinear equations.
Declare with attribute [code nbe].
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-- next part --
A non-text attachment w
> Proofs are much more fragile, notably unstructured ones. One way around
> this is to submit theory libraries and applications to
> http://afp.sourceforge.net/ where they get updated to latest Isabelle
> automagically.
Thanks to all the magicians ;-)
Florian
--
PGP available:
http
> While we're at it: what is the general feeling towards migrating the AFP
> to svn?
I have no strict opinion on this. Perhaps, if somebody wants to invest
the effort, there are no urgent causes against migrating to SVN. But if
not, staying with CVS is no desaster at all.
Florian
--
Some years ago two further constants were introduces into HOL.thy:
"undefined" and "default". The idea then was to divide the role of
classical "arbitrary" on two shoulders: "undefined" should be
unspecified an could be used to fake partiality, whereas "default" would
be overloaded and could be i
>> I wonder whether it is wise to have three of these. People are going to
>> attach more significance to them than they deserve. I am inclined to
>> think that we should get rid of arbitrary.
>> Larry
I also think that two would be better than three; technically
"undefined" is the same as "arbit
> Then what is the point of
>
> undefined_fun: "undefined x = undefined"
>
> in HOL.thy?
This is essentially pointless and is so soon to be dropped that I didn't
take the effort to even point out to it in my emails, taking the risk
that somebody would have a look a the source ;-)
Flo
* Unified theorem tables for both code code generators. Thus [code
func] has disappeared and only [code] remains. INCOMPATIBILITY.
--=20
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de
-- next part --
A n
Amine Chaieb schrieb:
> Dear all,
>
> (How) Can I perform an instantiation of a type-constructor with two
> arguments, an thereby restricting them to be the same?
This is beyond the type class system of Isabelle. A pity.
Florian
--
http://isabelle.in.tum.de/~haftmann
PGP available:
h
> :( I also failed a few weeks ago to instantiate the fold combinator to
> iterate function composition ...
Hmmm... perhaps "fold (op o) id id" is what you want in that case.
> But is this restriction fundamental or does it happen to be there?
Well, the type classes in Isabelle are an instance o
The switch to hg makes it possible to adapt some file locations (file
names) in the Isabelle distribution which have evolved over time but do
not fit to the logical structure of the distribution any longer,
according to the following table:
src/Provers/* ~> src/Tools/*
src/Pure/Tools/* ~>
Hi Brian,
> Is there any good reason why the constants "neg" and "iszero" (defined
> in Int.thy) are needed anymore?
if there is a chance to get rid of those, go ahead and try. Perhaps
they play a role for numerals and natural numbers, but this is just a
suspicion.
Cheers
Florian
--
Dear all,
let me add some observations:
> Actually, I had executability in mind when creating this theory. A new
> feature, which is not present in the original HOL/Abstract/poly development,
> is the constructor function pCons :: 'a => 'a poly => 'a poly. It basically
> means the same thing a
Type class package now uses new locale implementation.
Now need to tinker around with "class_interpretation" etc. any longer.
Florian
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenche
> wenzelm 1495934
>
> paulson 982335
> ***
> haftmann 413881 **
> nipkow 261461
Hi Amine,
I guess you are in the following thygraph situation:
Typrep Real
| / \ |
|/\|
Complex_Main FPS
\ /
\/
\ /
Foo
Real defines type real, Typerep class typerep (;-)). Then both in
Complex_Main and FPS and instance for ty
Hi all over there,
some comments on my behalf:
a) The Typerep theory if used by Imperative_HOL, but this is *not* its
only application; it is also used for evaluation using code generation
(value [code]) -- indeed, I added this immediately after the 2008
release in order to gain some experience h
Hi Amine,
> wrt to d) and e) (Users/Developers, HOL is difficult).
> This theory is for now a "using" HOL, but of course I want to develop it
> in a manner that it could become part of HOL.
> The situation you mention in d) and e) has not to be this way and we
> should not take it for granted that
minimal risk of producing "bad" thygraphs.
Florian
Florian Haftmann schrieb:
> Hi Amine,
>
>> wrt to d) and e) (Users/Developers, HOL is difficult).
>> This theory is for now a "using" HOL, but of course I want to develop it
>> in a manner t
* Class declaration: sc. "base sort" must not be given in import list
any longer but is inferred from the specification. Particularly in HOL,
write
class foo = ... instead of class foo = type + ...
Florian
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http:/
Hi Amine,
sorry for the inconvenience. Currently there is major upheaval going on
in the locale/class area. Im working hard on solving the remaining
problems.
For the moment I suggest going back to an earlier snapshot, e.g.
http://isabelle.in.tum.de/repos/isabelle/rev/bb0f395db245
Chers,
Hi Amine,
> For now HOL/Fact.thy defines factorials (over natural numbers) and
> strangely imports the reals. The theorem involving the reals, however,
> hold in any (ordered) (ring/field) of charachteristic Zero.
>
> Apart from that, I have a formalization of Pochhammer's symbol (raising
> facto
Hi Amine,
> I left Fact.thy alone because it is necessary for building HOL. I moved
> it upwards though (now it imports Nat instead of RealDef). I added the
> other stuff to Binomial since it is "Library stuff" and not necessary
> for building HOL.
OK, I see. This would even suggest to merge Fac
Dear Isabelle developers,
we are now heading towards the next Isabelle release.
Since Isabelle 2008 a lot of changes and improvements have found their
way into the sources. For this reason I would kindly invite you all to
update the NEWS and CONTRIBUTORS in the root of the repository to
document
Hi Amine,
> I have a theory development which used to work not a long time ago. I am
> now trying to include it into the distribution.
>
> At some point I can not merge the theories and get:
>
> *** Clash of specifications "Permutations.typerep_^_inst.typerep_^_def"
> and "Misc.typerep_^_inst.ty
tions import Main,
> the problem persists.
>
>
>
> Florian Haftmann wrote:
>> Hi Amine,
>>
>>> I have a theory development which used to work not a long time ago. I am
>>> now trying to include it into the distribution.
>>>
>>>
at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co
> work/Lib
>
> The files are then under Multivariate.
>
> Amine.
>
> PS: Please forgive for still using cvs, but I am applying the first
> commandment of Computer science.
>
> Florian Haftmann wrote:
>> Ca
I have to bother you further:
it is necessary to unfold the [HOL] node in the graph (by clicking on
it) because we need to inspect the internal structure of the HOL theories.
Florian
Amine Chaieb schrieb:
>
>
> Florian Haftmann wrote:
>> Amine Chaieb schrieb:
>>&
OK, seems like you have to change the following:
a) add Fact to the imports of Plain
b) add Main to the imports of Infinite_Set
and to the imports of Finite_Cartesian_Products
Our current policy is the Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
Hope this he
> Please do not give me fish but teach me how to fish!
Hmmm... I had been thinking I was doing both:
the fish...
>> a) add Fact to the imports of Plain
>> b) add Main to the imports of Infinite_Set
>> and to the imports of Finite_Cartesian_Products
and the fishing rules...
>> Our current pol
Our current policy is that Plain, Main (and Complex_Main) are either
ancestors or descendants of any theory.
> This rule does not tell me anything since it is trivally satisfied by
> any connected graph containing Plain, Main and Complex_Main.
The rule rules out the following situation:
Hi Clemens,
> I would like to hear of any problems that are due to the new locales
> implementation. So far, I have not received any messages, but I have
> seen that modifications to fairly intricate parts were made.
Those problems this e-mail conversation has referred to were about
reading clas
Hi Brian,
>> Our current policy is the Plain, Main and Complex_Main are either
>> ancestors or descendants of any theory.
>
> OK, the requirement for Plain I can understand. For Main, it doesn't
> seem too unreasonable, assuming it's necessary (since most theory files
> import Main anyway).
>
>
Dear all,
I think there are different aspects which we should clearly set apart.
a) Keeping theory imports minimal vs. reducing the number of merges
Careful thinking what the logical preliminaries of a particular theory
are is a necessary, valuable and fruitful task -- I would by no means
encour
Hi Brian,
> I'm afraid I don't understand why reducing the number of merges by
> adding "wasp-waists" is beneficial. From what I understand, adding
> additional theory dependencies could only reduce opportunities for
> parallel execution. Is there another technical reason why the amount of
> mergi
Hi Brian,
> The following code works:
>
> datatype 'a bintree = Branch "'a bintree" "'a bintree" | Tip 'a
> definition "test1 = (Tip True = Branch (Tip False) (Tip True))"
> export_code test1 in Haskell file -
>
> but this other example doesn't:
>
> datatype 'a tree = Node 'a "'a tree list"
> d
Hi Brian,
> However, if I try to generate OCaml or SML code, the second one still
> fails, but with a different error this time:
>
> *** Illegal mutual dependencies: "tree :: eq", "eq_class.eq [tree]"
> *** At command "export_code".
>
> What do you think?
This is the situation as reported in se
Hi Brian,
> Sometimes the "class" command can be rather slow, for example:
> I don't know what the "class" command is doing behind the scenes, but is
> it supposed to be taking this long? Should this be considered a
> performance bug?
Without a closer look at this I would deem that this is due t
Dear Amine and Jeremy,
the current development snapshot now has fixed the problem. Switching
to it should be rather safe -- we plan to converge to the next Isabelle
release quite soon and refrain from major changes.
Thanks for your patience. There are still minor issues which I have to
reorgani
> New predicate "strict_mono" classifies strict functions on partial orders.
> With strict functions on linear orders, reasoning about (in)equalities is
> facilitated by theorems "strict_mono_eq", "strict_mono_eq" and
> "strict_mono_eq".
Florian
--
Home:
http://wwwbroy.in.tum.de/~haftm
Amine Chaieb schrieb:
>
> Florian,
>
>> facilitated by theorems "strict_mono_eq", "strict_mono_eq" and
>> "strict_mono_eq".
should have been "strict_mono_eq", "strict_mono_less_eq", "strict_mono_less"
;-) Florian
P.S. Even today we are facing difficult problems, which are very
difficul
lemma "\m n x. x \ P \ Suc (2 * m) = 2 * n
\ False"
apply presburger done
lemma "\m n x. P x \ Suc (2 * m) = 2 * n
\ False"
apply presburger -- fails
This phenomenon already occurs in Isabelle 2008 and still persists. The
confusing fact is that neither x nor P matter anyway.
Any idea?
I have distilled another problem which definitely has nothing to do with
atomization:
lemma "\(x\'a::type) m n.
P x \ Suc (2 * m) = 2 * n \ False"
apply (atomize (full))
apply presburger
done
lemma "\(x\'a::type) m n.
Q x \ P x \ Suc (2 * m) = 2 * n
\ False"
apply (atomize (
People who are not constantly busy with the Isabelle repository itself
will hardly follow each changeset explicitly. Then I recommend to use
hg update with verbose flag:
hg update -v
resp.
hg pull -u -v
This then imitates the CVS style output which tells explicitly which
files
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
Florian
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_t
* Power operations on relations and functions are now one dedicate
constant compow with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic in
class recpower; class power disappeared. INCOMPATIBILITY.
NOTE: This needs not to be the last wo
> What happened to this option? I cannot run one of my draft papers
> anymore. How do I have to write it these days? I couldn't find anything
> in NEWS.
text (in ...) {* ... @{thm ...} *}
should work.
It could be the case that the locale= option was never part of an
official release and thus has
Hi Brian,
> I'm just wondering about why the "class" command is an improvement
> over "axclass" in this situation:
>
> http://isabelle.in.tum.de/repos/isabelle/rev/d1cb222438d8
Perhaps not "improvement", but "replacement"; before Isabelle 2009,
there were still situations which "class" could no
> thanks for reporting this. I hope to eliminate this problem within this
> day.
http://isabelle.in.tum.de/repos/isabelle/shortlog
Done
Florian
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 byt
Hi Brian,
thanks for reporting this. I hope to eliminate this problem within this
day.
Hope this helps,
Florian
Brian Huffman schrieb:
> Hi all,
>
> I recently tried to make some changes to the topological_space class
> in RealVector.thy (I moved the definition of "open" here from
> Li
Discontinued ancient tradition to suffix certain ML module names with
"_package", e.g.:
DatatypePackage ~> Datatype
InductivePackage ~> Inductive
etc.
Florian
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/flor
Hi Amine,
> *** Clash of specifications "Sign.sign.size_sign_inst.size_sign_def" and
> "Sign.sign.size_sign_inst.size_sign_def" for constant "Nat.size_class.size"
> *** At command "theory".
I guess that you have a theory which introduces a type "sign". When you
ensure that this theory has "Plain
Hi Lucas,
> apply (unfold Product_Type.pair_collapse[symmetric, of "al"])
The equation Product_Type.pair_collapse[symmetric, of "al"] can be
unfolded forever, so the method invocation does not terminate, leading
to an unspecified behaviour of the system!
As a quick replacement, consider
Hi Walter,
> Why is NumeralSyntax.setup available in HOL/Int.thy, but not in the
> Isabelle/HOL ML toplevel ? ...
>
> ML> NumeralSyntax.setup;
> Error-Structure (NumeralSyntax) has not been declared Found near
> NumeralSyntax.setup
the reason for this is that Isabelle administrates the ML name
Hi Lucas,
indeed the whole quickcheck matter has grown into a complex story.
First, we currently (e.g. following development in the hg repository)
have a kind of fork: there is the "old" quickcheck, residing in
Pure/codegen.ML, and the "new" one in HOL/Quickcheck.thy; the most
prominent differen
Hi Lucas,
perhaps the source of the confusion can be found here:
http://isabelle.in.tum.de/repos/isabelle/file/6b31b143f18b/src/Pure/codegen.ML
I.e. due to a misunderstanding of interfacing convention (0 is also a
valid size), Codegn.test_term in Isabelle2009 would increase its size
argument by
Changes culminated over the last 12 months:
Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with
le_inf_iff
- dropped l
1 - 100 of 901 matches
Mail list logo
