src/HOL/Tools/inductive.ML
Sat, 19 Nov 2011 21:18:38 +0100 wenzelm added ML antiquotation @{attributes};
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Sat, 10 Sep 2011 19:44:41 +0200 haftmann more modularization
Wed, 27 Apr 2011 20:19:05 +0200 wenzelm more precise position information via Variable.add_fixes_binding;
Wed, 20 Apr 2011 22:57:29 +0200 wenzelm eliminated Display.string_of_thm_without_context;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn tuned
Wed, 03 Nov 2010 11:06:22 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
less more (0) -15 tip