Tue, 27 Mar 2007 17:54:37 +0200 berghofe Exported perm_of_pair, mk_not_sym, and perm_simproc.
Tue, 27 Mar 2007 12:28:42 +0200 haftmann cleaned up HOL/ex/Code*.thy
Tue, 27 Mar 2007 09:19:37 +0200 haftmann fixed document preparation
Mon, 26 Mar 2007 16:35:33 +0200 krauss fixed problem with mutual recursion
Mon, 26 Mar 2007 14:54:45 +0200 haftmann cleaned up Library/ and ex/
Mon, 26 Mar 2007 14:53:07 +0200 haftmann minimal intro rules
Mon, 26 Mar 2007 14:53:06 +0200 haftmann exported interface for intro rules
Mon, 26 Mar 2007 14:53:05 +0200 haftmann moved Eval theory to library
Mon, 26 Mar 2007 14:53:04 +0200 haftmann Eval theory
Mon, 26 Mar 2007 14:53:03 +0200 haftmann tuned
Mon, 26 Mar 2007 14:53:02 +0200 haftmann importing Eval theory
Mon, 26 Mar 2007 14:53:01 +0200 haftmann naming tuned
Mon, 26 Mar 2007 14:53:00 +0200 haftmann cleaned up Library( and ex/
Mon, 26 Mar 2007 12:48:30 +0200 paulson Clause cache is now in theory data.
Mon, 26 Mar 2007 12:46:27 +0200 paulson "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
Sun, 25 Mar 2007 15:15:07 +0200 urbanc moving lemmas into appropriate sections
Fri, 23 Mar 2007 12:06:41 +0100 haftmann fixed typing bug in generated code
Fri, 23 Mar 2007 12:05:43 +0100 haftmann fixed typing bug in generated code
Fri, 23 Mar 2007 10:50:03 +0100 urbanc added the permutation operation on options to the list of equivariance lemmas
Fri, 23 Mar 2007 09:46:22 +0100 haftmann dropped
Fri, 23 Mar 2007 09:40:57 +0100 haftmann added empty cases
Fri, 23 Mar 2007 09:40:53 +0100 haftmann added concept for term constructors
Fri, 23 Mar 2007 09:40:50 +0100 haftmann tuned
Fri, 23 Mar 2007 09:40:49 +0100 haftmann two further properties about lists
Fri, 23 Mar 2007 09:40:47 +0100 haftmann removed outdated example
Fri, 23 Mar 2007 09:40:45 +0100 haftmann fixed typo
Fri, 23 Mar 2007 09:40:43 +0100 haftmann added some sketches about library functions
Thu, 22 Mar 2007 16:53:37 +0100 krauss fixed function syntax
Thu, 22 Mar 2007 16:34:03 +0100 krauss fixed function syntax
Thu, 22 Mar 2007 14:26:05 +0100 urbanc corrected the lemmas min_nat_eqvt and min_int_eqvt
Thu, 22 Mar 2007 14:03:30 +0100 haftmann fixed code generator setup
Thu, 22 Mar 2007 13:36:57 +0100 krauss made function syntax strict, requiring | to separate equations; cleanup
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
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip