Thu, 29 Mar 2007 14:21:47 +0200 haftmann improved character output for SML
Thu, 29 Mar 2007 14:21:45 +0200 haftmann dropped legacy ML bindings
Thu, 29 Mar 2007 11:59:54 +0200 paulson simplified some steps
Thu, 29 Mar 2007 11:12:39 +0200 paulson MESON tactical takes an additional argument: the clausification function.
Thu, 29 Mar 2007 11:12:03 +0200 paulson Now checks for types-only clause before outputting.
Wed, 28 Mar 2007 19:18:39 +0200 berghofe - Improved error messages in equivariance proof
Wed, 28 Mar 2007 19:17:40 +0200 berghofe Renamed induct(s)_weak to weak_induct(s) in order to unify
Wed, 28 Mar 2007 19:16:11 +0200 berghofe - Renamed <predicate>_eqvt to <predicate>.eqvt
Wed, 28 Mar 2007 18:25:23 +0200 urbanc the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
Wed, 28 Mar 2007 17:27:44 +0200 urbanc adapted to new nominal_inductive
Wed, 28 Mar 2007 10:47:19 +0200 berghofe Improved code generator for characters: now handles
Wed, 28 Mar 2007 01:55:18 +0200 urbanc tuned proofs (taking full advantage of nominal_inductive)
Wed, 28 Mar 2007 01:29:43 +0200 urbanc adapted to nominal_inductive infrastructure
Wed, 28 Mar 2007 01:09:23 +0200 urbanc made the type sets instance of the "cp" type-class
Tue, 27 Mar 2007 19:39:40 +0200 urbanc added extended the lemma for equivariance of freshness
Tue, 27 Mar 2007 19:13:28 +0200 urbanc adapted to nominal_inductive
Tue, 27 Mar 2007 18:28:22 +0200 urbanc adapted to new nominal_inductive infrastructure
Tue, 27 Mar 2007 17:57:42 +0200 berghofe Adapted to new syntax of nominal_inductive.
Tue, 27 Mar 2007 17:57:05 +0200 berghofe Adapted to changes in nominal_inductive.
Tue, 27 Mar 2007 17:55:09 +0200 berghofe Implemented proof of strong induction rule.
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
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip