krauss [Thu, 22 Mar 2007 13:36:57 +0100] rev 22498
made function syntax strict, requiring | to separate equations; cleanup
krauss [Thu, 22 Mar 2007 13:36:56 +0100] rev 22497
fixed problem with the construction of mutual simp rules
krauss [Thu, 22 Mar 2007 13:36:55 +0100] rev 22496
cleanup
urbanc [Thu, 22 Mar 2007 11:17:32 +0100] rev 22495
clarified an error-message
urbanc [Thu, 22 Mar 2007 10:35:12 +0100] rev 22494
tuned some proofs
krauss [Wed, 21 Mar 2007 16:07:40 +0100] rev 22493
added another rule for simultaneous induction, and lemmas for zip
krauss [Wed, 21 Mar 2007 16:06:15 +0100] rev 22492
Unified function syntax
paulson [Wed, 21 Mar 2007 13:58:36 +0100] rev 22491
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
haftmann [Wed, 21 Mar 2007 08:07:19 +0100] rev 22490
added example file
gagern [Tue, 20 Mar 2007 21:21:38 +0100] rev 22489
Better documentation path rewriting for src dir, used in tarball build.
gagern [Tue, 20 Mar 2007 20:42:14 +0100] rev 22488
Changed AnnoMaLy build process from CVS to tarball sources.
Moved annomaly.ML from the official sources to the isatest directory.
krauss [Tue, 20 Mar 2007 17:07:23 +0100] rev 22487
simplified "eval" oracle method
haftmann [Tue, 20 Mar 2007 15:52:43 +0100] rev 22486
updated keywords
haftmann [Tue, 20 Mar 2007 15:52:42 +0100] rev 22485
added theory dependency graph
haftmann [Tue, 20 Mar 2007 15:52:41 +0100] rev 22484
improved treatment of defining equations stemming from specification tools
haftmann [Tue, 20 Mar 2007 15:52:40 +0100] rev 22483
added instance for lattice
haftmann [Tue, 20 Mar 2007 15:52:39 +0100] rev 22482
dropped OrderedGroup.ML
haftmann [Tue, 20 Mar 2007 15:52:38 +0100] rev 22481
added class "default" and expansion axioms for undefined
haftmann [Tue, 20 Mar 2007 15:52:37 +0100] rev 22480
switched exception from arbitrary to undefined
haftmann [Tue, 20 Mar 2007 10:23:31 +0100] rev 22479
updated code generation sections
haftmann [Tue, 20 Mar 2007 08:27:23 +0100] rev 22478
fixed typo
haftmann [Tue, 20 Mar 2007 08:27:22 +0100] rev 22477
new lemmas
haftmann [Tue, 20 Mar 2007 08:27:21 +0100] rev 22476
pretty function arrow for diag serializer
haftmann [Tue, 20 Mar 2007 08:27:20 +0100] rev 22475
adjusted definition of defining equation
haftmann [Tue, 20 Mar 2007 08:27:19 +0100] rev 22474
fixed slip
haftmann [Tue, 20 Mar 2007 08:27:15 +0100] rev 22473
explizit "type" superclass
urbanc [Mon, 19 Mar 2007 19:28:27 +0100] rev 22472
tuned the proof
paulson [Mon, 19 Mar 2007 15:58:02 +0100] rev 22471
Removal of axiom names from the theorem cache
paulson [Mon, 19 Mar 2007 15:57:20 +0100] rev 22470
No label on "show"; tries to remove dependencies more cleanly
haftmann [Mon, 19 Mar 2007 11:59:36 +0100] rev 22469
dropped overwrite_warn