src/HOL/Tools/record.ML
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;
Sat, 17 Oct 2009 20:37:38 +0200 wenzelm removed separate record_quick_and_dirty_sensitive;
Sat, 17 Oct 2009 20:15:59 +0200 wenzelm simplified tactics;
Sat, 17 Oct 2009 19:04:35 +0200 wenzelm eliminated old List.foldr and OldTerm operations;
Sat, 17 Oct 2009 18:14:47 +0200 wenzelm removed unused names;
Sat, 17 Oct 2009 18:01:24 +0200 wenzelm misc tuning and simplification;
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Thu, 01 Oct 2009 14:11:28 +0200 wenzelm avoid mixed l/r infixes, which do not work in some versions of SML;
Thu, 01 Oct 2009 12:15:35 +0200 wenzelm tuned;
Thu, 01 Oct 2009 01:03:36 +0200 wenzelm eliminated dead code, redundant bindings and parameters;
Wed, 30 Sep 2009 00:27:19 +0200 wenzelm made SML/NJ happy;
Tue, 29 Sep 2009 23:14:57 +0200 wenzelm removed dead/duplicate code;
Tue, 29 Sep 2009 22:48:24 +0200 wenzelm modernized Balanced_Tree;
Tue, 29 Sep 2009 22:33:27 +0200 wenzelm replaced meta_iffD2 by existing Drule.equal_elim_rule2;
Tue, 29 Sep 2009 21:36:49 +0200 wenzelm tuned header;
Tue, 29 Sep 2009 21:34:59 +0200 wenzelm tuned whitespace -- recover basic Isabelle conventions;
Tue, 29 Sep 2009 18:14:08 +0200 wenzelm merged
Tue, 29 Sep 2009 14:25:42 +1000 Thomas Sewell Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
Mon, 28 Sep 2009 15:37:19 +1000 Thomas Sewell Avoid a possible variable name conflict in instantiating a theorem.
Wed, 23 Sep 2009 19:17:48 +1000 tsewell Initial response to feedback from Norbert, Makarius on record patch
Fri, 11 Sep 2009 20:58:29 +1000 Thomas Sewell Implement previous fix (don't duplicate ext_def) correctly.
Fri, 11 Sep 2009 18:03:30 +1000 Thomas Sewell There's no particular reason to duplicate the extension
Thu, 10 Sep 2009 16:38:18 +1000 Thomas Sewell Simplification of various aspects of the IsTuple component
Thu, 10 Sep 2009 15:18:43 +1000 Thomas Sewell Record patch imported and working.
Thu, 27 Aug 2009 00:40:53 +1000 tsewell Initial attempt at porting record update to repository Isabelle.
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 07 Aug 2009 19:16:04 +0200 wenzelm tuned spacing of sections;
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Sun, 26 Jul 2009 20:38:11 +0200 wenzelm replaced old METAHYPS by FOCUS;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
less more (0) tip