NEWS
Wed, 14 Mar 2012 11:45:16 +0100 wenzelm Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
Tue, 13 Mar 2012 16:22:18 +0100 wenzelm improved attribute "abs_def" to handle object-equality as well;
Mon, 12 Mar 2012 21:34:45 +0100 noschinl NEWS
Wed, 07 Mar 2012 21:38:29 +0100 haftmann less rigorous but more realistic migration recommendation; note on code generation of sets
Thu, 01 Mar 2012 19:34:52 +0100 haftmann more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
Tue, 28 Feb 2012 15:54:51 +0100 blanchet spelling
Fri, 24 Feb 2012 11:23:34 +0100 blanchet renamed 'try_methods' to 'try0'
Wed, 22 Feb 2012 18:08:27 +0100 bulwahn NEWS
Sat, 18 Feb 2012 23:05:31 +0100 krauss NEWS
Fri, 17 Feb 2012 15:42:26 +0100 wenzelm simplified configuration options for syntax ambiguity;
Thu, 16 Feb 2012 22:18:28 +0100 wenzelm simplified configuration options for syntax ambiguity;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 15 Feb 2012 21:08:27 +0100 wenzelm discontinued obsolete "prems" fact;
Wed, 15 Feb 2012 19:31:27 +0100 wenzelm NEWS;
Wed, 15 Feb 2012 13:24:22 +0100 wenzelm renamed "xstr" to "str_token";
Tue, 14 Feb 2012 16:59:12 +0100 wenzelm tuned;
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments)
Tue, 31 Jan 2012 07:11:04 +0100 nipkow NEWS
Mon, 30 Jan 2012 17:15:59 +0100 blanchet docs and news
Mon, 30 Jan 2012 13:55:28 +0100 bulwahn NEWS
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict"
Tue, 17 Jan 2012 11:15:36 +0100 bulwahn refreshing NEWS
Mon, 16 Jan 2012 21:50:15 +0100 wenzelm position constraints for numerals enable PIDE markup;
Tue, 10 Jan 2012 10:48:39 +0100 bulwahn NEWS
Mon, 09 Jan 2012 14:47:18 +0100 wenzelm misc tuning and reformatting;
Fri, 06 Jan 2012 21:48:45 +0100 haftmann consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
Fri, 06 Jan 2012 10:53:52 +0100 haftmann more explicit NEWS
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
Thu, 05 Jan 2012 20:26:01 +0100 wenzelm discontinued Syntax.positions -- atomic parse trees are always annotated;
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Wed, 28 Dec 2011 12:55:37 +0100 huffman fix typos
Wed, 28 Dec 2011 12:52:23 +0100 huffman remove some duplicate lemmas
Tue, 27 Dec 2011 09:15:26 +0100 haftmann be explicit about Finite_Set.fold
Mon, 26 Dec 2011 22:17:10 +0100 haftmann NEWS: unavoidable fact renames
Sat, 24 Dec 2011 16:14:59 +0100 haftmann NEWS: `set` is now a proper type constructor
Fri, 23 Dec 2011 15:55:23 +0100 huffman remove redundant lemma word_sub_def
Wed, 21 Dec 2011 09:39:14 +0100 bulwahn NEWS
Wed, 14 Dec 2011 17:49:42 +0100 bulwahn NEWS
Tue, 13 Dec 2011 23:23:51 +0100 wenzelm 'datatype' specifications allow explicit sort constraints;
Sat, 10 Dec 2011 22:00:42 +0100 huffman prove class instances without extra lemmas
Fri, 09 Dec 2011 14:52:51 +0100 huffman remove redundant lemma word_diff_minus
Fri, 09 Dec 2011 11:31:13 +0100 noschinl more systematic lemma name
Mon, 05 Dec 2011 12:36:03 +0100 bulwahn NEWS
Sun, 04 Dec 2011 13:10:19 +0100 huffman remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice"
Thu, 01 Dec 2011 12:25:27 +0100 wenzelm renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Mon, 21 Nov 2011 23:29:53 +0100 wenzelm NEWS;
Sun, 20 Nov 2011 17:44:41 +0100 wenzelm 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
Sat, 19 Nov 2011 21:23:16 +0100 wenzelm NEWS;
Sat, 19 Nov 2011 21:18:38 +0100 wenzelm added ML antiquotation @{attributes};
Thu, 17 Nov 2011 15:07:46 +0100 huffman HOL-Word: removed more duplicate theorems
Thu, 17 Nov 2011 14:52:05 +0100 huffman HOL-Word: removed many duplicate theorems (see NEWS)
Wed, 16 Nov 2011 10:34:08 +0100 blanchet document "lam_trans" option
Wed, 09 Nov 2011 17:57:42 +0100 wenzelm sort assignment before simultaneous term_check, not isolated parse_term;
Mon, 07 Nov 2011 22:22:01 +0100 blanchet avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
Mon, 07 Nov 2011 14:23:50 +0100 wenzelm clarified attribute "mono_set": pure declaration, proper export in ML;
less more (0) -1000 -300 -100 -60 tip