Actually, there is a third code generator hidden somewhere in Isabelle.
- Steven
On 21.07.2011, at 12:18, Lukas Bulwahn wrote:
> Hello all,
>
>
> at the moment, we have two code generators in Isabelle:
>
> 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML
> withou
Lukas already assured me of that. No worries here.
- Steven
On 22.07.2011, at 00:07, Alexander Krauss wrote:
> On 07/21/2011 04:25 PM, Steven Obua wrote:
>> Actually, there is a third code generator hidden somewhere in
>> Isabelle.
>
> If you are talking about what
>
>
> Anyway, since eq_reflection actually *is* an axiom, and (=) actually
> *does* mean the same thing as (==), then I really don't see any reason
> why we need to have both (or separate bool and prop types, for that
> matter). I don't know of any other HOL provers that do.
>
> Even if we got rid
>
> In the translation to ZF which Andy and I am developing, such
> "strange proofs" actually caused some weird problems at some point.
This sounds interesting :-) Is there more information on this
translation available?
Best,
Steven
PS: For those of you who a) speak German b) play Skat c)
>
> NatBin.thy is now nearly "neg"-free, but there are still some other
> places with lemmas that use "neg". For example, Tools/
> ComputeNumeral.thy seems to be a complete re-implementation of the
> simpset defined in NatBin.thy for arithmetic at type nat. If such
> other lemmas involving "
I just came across this great new language for the Java VM, Clojure. It
is like somebody read my mind about how a modern programming language
should be, melted the vague ideas there into a detailed specification,
put a lot of other goodies like STM in there, and finally implemented it!
I recom
Makarius wrote:
>This is because token translations are only used when printing terms, not
>when presenting theory sources.
>
>
>
Yes, I noticed that.
Is there any quick hack around it ?
Steven
Hi,
I am using the Isar token translation mechanism to modify the latex
generation of Isabelle.
token_translation {*
.
*}
This works fine if if output stuff for example like that
text{*
@{thm float_add}
*}
But it does not work for the main output of a theory, like
lemma "balabla"
sor
Hi,
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-Complex-
Hi,
until shortly before the Isabelle2007 release the following line worked:
lemmas find_simp = While_simp[where continue="(\ x. ?f x
\ x)", simplified find_def[symmetric]]
Now it complains that the schematic variable ?f is not allowed. This
variable occurs in While_simp, too, and I want to sp
Amine Chaieb wrote:
>LCF? are you kidding?
>
>
So how did you do it then ? How long did the check run? Where can I find
the sources?
Steven
I am experiencing a major breakdown of performance after updating my
Isabelle system. I am using large records and locales, could this be
the reason? Oddly, while it takes longer than expected to parse a
record declaration, the real problem seems to be the statement of
lemmas after it (not ev
Hi,
ich habe gerade Isabelle geupdatet auf meinem Rechner. Leider l?uft
jetzt eine Theorie bei mir nicht mehr durch (und damit auch alles andere
was ich so f?r meine t?gliche Arbeit brauche :-( )
Und zwar:
Ich lade die Theorie mit 'use_thy "While"'. Nachdem ALLE lemmas in der
Theorie erfolgre
http://www.artima.com/forums/flat.jsp?forum=278&thread=217150
Hi,
I have the following setup:
(1) a theory "lemmas.thy"
(2) some ML-code that uses this theory and that is loaded and executed
after the theory has been loaded
(3) some additional ML-code that defines a function f
I now use f and suddenly I notice that I have to update lemmas.thy by
for exam
15 matches
Mail list logo
