src/HOL/Tools/record.ML
Sat, 19 Jun 2010 09:50:30 +0200 haftmann more binding; avoid arcane Rep and Abs prefixes
Sat, 19 Jun 2010 09:14:06 +0200 haftmann cleanup of typecopy package
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Wed, 26 May 2010 16:05:25 +0200 haftmann dropped legacy theorem bindings
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 16 Apr 2010 19:58:04 +0200 wenzelm modernized type abbreviations;
Thu, 15 Apr 2010 21:24:00 +0200 wenzelm more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);
Thu, 15 Apr 2010 18:09:22 +0200 wenzelm replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
Thu, 15 Apr 2010 16:58:12 +0200 wenzelm modernized treatment of sort constraints in specification;
Wed, 14 Apr 2010 16:15:19 +0200 krauss record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
Sat, 27 Mar 2010 21:38:38 +0100 wenzelm Typedef.info: separate global and local part, only the latter is transformed by morphisms;
Sat, 27 Mar 2010 18:07:21 +0100 wenzelm moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
Sat, 13 Mar 2010 14:43:04 +0100 wenzelm global typedef;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sat, 06 Mar 2010 17:32:45 +0100 wenzelm record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
Sat, 06 Mar 2010 16:13:22 +0100 wenzelm record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
Wed, 03 Mar 2010 00:32:14 +0100 wenzelm adapted to authentic syntax -- actual types are verbatim;
Sun, 28 Feb 2010 23:51:31 +0100 wenzelm more antiquotations;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Thu, 25 Feb 2010 22:17:33 +0100 wenzelm explicit @{type_syntax} markup;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Fri, 19 Feb 2010 22:06:01 +0100 wenzelm tuned;
Fri, 19 Feb 2010 21:31:14 +0100 wenzelm authentic term syntax;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Tue, 16 Feb 2010 20:41:52 +0100 wenzelm simplified/clarified record print translations;
Tue, 16 Feb 2010 16:42:18 +0100 wenzelm eliminated camel case;
Tue, 16 Feb 2010 16:40:16 +0100 wenzelm tuned;
Tue, 16 Feb 2010 16:03:06 +0100 wenzelm simplified/clarified record translations;
Tue, 16 Feb 2010 14:08:39 +0100 wenzelm moved generic update_name to Pure syntax -- not specific to HOL/record;
Tue, 16 Feb 2010 13:35:42 +0100 wenzelm tuned;
Tue, 16 Feb 2010 13:06:43 +0100 wenzelm conceal internal record definitions;
Mon, 15 Feb 2010 23:58:24 +0100 wenzelm refined and exported record_info;
Mon, 15 Feb 2010 22:40:03 +0100 wenzelm modernized structures;
Mon, 15 Feb 2010 22:24:19 +0100 wenzelm modernized signature -- proper binding;
Mon, 15 Feb 2010 20:32:21 +0100 wenzelm tuned errors;
Mon, 15 Feb 2010 20:01:07 +0100 wenzelm formal markup of constants;
Mon, 15 Feb 2010 18:50:16 +0100 wenzelm eliminated old fold;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Mon, 21 Dec 2009 08:32:04 +0100 haftmann prefer prefix "iso" over potentially misleading "is"; tuned
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Mon, 16 Nov 2009 13:49:21 +0100 wenzelm guard future proofs by Goal.future_enabled;
Sat, 14 Nov 2009 09:31:54 +0100 schirmer clarified quick-and-dirty usage in record package;
Wed, 11 Nov 2009 15:10:26 +0100 haftmann adding code equations for constructors
Tue, 10 Nov 2009 16:11:43 +0100 haftmann substantial simplification restores code generation
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Mon, 02 Nov 2009 20:38:46 +0100 wenzelm modernized structure Primitive_Defs;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Wed, 21 Oct 2009 16:57:57 +0200 blanchet merged
Wed, 21 Oct 2009 16:53:00 +0200 blanchet removed "nitpick_const_simp" attribute from Record's "simps";
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 20 Oct 2009 20:54:31 +0200 wenzelm uniform use of Integer.min/max;
Sat, 17 Oct 2009 21:14:08 +0200 wenzelm tuned;
less more (0) -60 tip