Thu, 22 Mar 2007 13:36:56 +0100 krauss fixed problem with the construction of mutual simp rules
Thu, 22 Mar 2007 13:36:55 +0100 krauss cleanup
Thu, 22 Mar 2007 11:17:32 +0100 urbanc clarified an error-message
Thu, 22 Mar 2007 10:35:12 +0100 urbanc tuned some proofs
Wed, 21 Mar 2007 16:07:40 +0100 krauss added another rule for simultaneous induction, and lemmas for zip
Wed, 21 Mar 2007 16:06:15 +0100 krauss Unified function syntax
Wed, 21 Mar 2007 13:58:36 +0100 paulson Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
Wed, 21 Mar 2007 08:07:19 +0100 haftmann added example file
Tue, 20 Mar 2007 21:21:38 +0100 gagern Better documentation path rewriting for src dir, used in tarball build.
Tue, 20 Mar 2007 20:42:14 +0100 gagern Changed AnnoMaLy build process from CVS to tarball sources.
Tue, 20 Mar 2007 17:07:23 +0100 krauss simplified "eval" oracle method
Tue, 20 Mar 2007 15:52:43 +0100 haftmann updated keywords
Tue, 20 Mar 2007 15:52:42 +0100 haftmann added theory dependency graph
Tue, 20 Mar 2007 15:52:41 +0100 haftmann improved treatment of defining equations stemming from specification tools
Tue, 20 Mar 2007 15:52:40 +0100 haftmann added instance for lattice
Tue, 20 Mar 2007 15:52:39 +0100 haftmann dropped OrderedGroup.ML
Tue, 20 Mar 2007 15:52:38 +0100 haftmann added class "default" and expansion axioms for undefined
Tue, 20 Mar 2007 15:52:37 +0100 haftmann switched exception from arbitrary to undefined
Tue, 20 Mar 2007 10:23:31 +0100 haftmann updated code generation sections
Tue, 20 Mar 2007 08:27:23 +0100 haftmann fixed typo
Tue, 20 Mar 2007 08:27:22 +0100 haftmann new lemmas
Tue, 20 Mar 2007 08:27:21 +0100 haftmann pretty function arrow for diag serializer
Tue, 20 Mar 2007 08:27:20 +0100 haftmann adjusted definition of defining equation
Tue, 20 Mar 2007 08:27:19 +0100 haftmann fixed slip
Tue, 20 Mar 2007 08:27:15 +0100 haftmann explizit "type" superclass
Mon, 19 Mar 2007 19:28:27 +0100 urbanc tuned the proof
Mon, 19 Mar 2007 15:58:02 +0100 paulson Removal of axiom names from the theorem cache
Mon, 19 Mar 2007 15:57:20 +0100 paulson No label on "show"; tries to remove dependencies more cleanly
Mon, 19 Mar 2007 11:59:36 +0100 haftmann dropped overwrite_warn
Mon, 19 Mar 2007 11:59:35 +0100 haftmann moved Output.overwrite_warn here
Sun, 18 Mar 2007 01:50:05 +0100 dixon TrueElim and notTrueElim tested and added as safe elim rules.
Fri, 16 Mar 2007 21:35:30 +0100 haftmann dropped LOrder.thy in favor of Lattices.thy
Fri, 16 Mar 2007 21:33:31 +0100 haftmann dropped LOrder.thy
Fri, 16 Mar 2007 21:32:22 +0100 haftmann added "satisfies" interface
Fri, 16 Mar 2007 21:32:21 +0100 haftmann dropping dead code
Fri, 16 Mar 2007 21:32:20 +0100 haftmann clarified check of defining equations
Fri, 16 Mar 2007 21:32:19 +0100 haftmann adjusted qualified thm reference
Fri, 16 Mar 2007 21:32:18 +0100 haftmann inf_fun_eq and inf_bool_eq now with meta equality
Fri, 16 Mar 2007 21:32:15 +0100 haftmann added "class"es
Fri, 16 Mar 2007 21:32:14 +0100 haftmann tuned
Fri, 16 Mar 2007 21:32:13 +0100 haftmann dropped superfluous hide
Fri, 16 Mar 2007 21:32:12 +0100 haftmann added lattice definitions
Fri, 16 Mar 2007 21:32:11 +0100 haftmann added instance of sets as distributive lattices
Fri, 16 Mar 2007 21:32:10 +0100 haftmann integrated with LOrder.thy
Fri, 16 Mar 2007 21:32:09 +0100 haftmann moved lattice instance here
Fri, 16 Mar 2007 21:32:08 +0100 haftmann adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
Fri, 16 Mar 2007 21:32:07 +0100 haftmann added FIXME hints
Fri, 16 Mar 2007 21:32:06 +0100 haftmann lattice cleanup
Fri, 16 Mar 2007 21:32:05 +0100 haftmann updated
Fri, 16 Mar 2007 17:17:36 +0100 urbanc adjusted for the example file SOS.thy
Fri, 16 Mar 2007 17:12:52 +0100 urbanc added formalisations of typical SOS-proofs
Fri, 16 Mar 2007 17:09:18 +0100 urbanc added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
Fri, 16 Mar 2007 16:40:49 +0100 dixon removed safe elim flag of trueElim and notFalseElim for testing.
Fri, 16 Mar 2007 16:37:52 +0100 dixon added safe intro rules for removing "True" subgoals as well as "~ False" ones.
Wed, 14 Mar 2007 21:52:26 +0100 huffman move sqrt_divide_self_eq to NthRoot.thy
Wed, 14 Mar 2007 21:40:28 +0100 huffman move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
Wed, 14 Mar 2007 01:35:02 +0100 webertj is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
Tue, 13 Mar 2007 08:49:58 +0100 urbanc deleted function for defining candidates and used nominal_primrec instead
Mon, 12 Mar 2007 19:23:49 +0100 wenzelm syntax: proper body priorty for derived binders;
Mon, 12 Mar 2007 19:23:48 +0100 wenzelm tuned;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip