src/HOL/Import/proof_kernel.ML
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
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
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Thu, 15 Oct 2009 23:10:35 +0200 wenzelm space_implode;
Thu, 15 Oct 2009 16:15:22 +0200 wenzelm sort_strings (cf. Pure/library.ML);
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 28 Aug 2009 21:04:03 +0200 wenzelm modernized messages -- eliminated ctyp/cterm operations;
Fri, 24 Jul 2009 22:31:27 +0200 wenzelm ML_Context.the_local_context;
Fri, 24 Jul 2009 21:02:34 +0200 wenzelm explicit OldGoals;
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.;
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Wed, 11 Mar 2009 15:56:49 +0100 haftmann stripped dead code
Sat, 07 Mar 2009 23:30:58 +0100 wenzelm minimal adaptions for abstract binding type;
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 21 Jan 2009 18:27:43 +0100 haftmann binding replaces bstring
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm eliminated OldTerm.(add_)term_consts;
Wed, 31 Dec 2008 20:31:36 +0100 wenzelm eliminated OldTerm.add_term_free_names;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 23 Oct 2008 15:28:39 +0200 wenzelm Thm.def_name;
Wed, 22 Oct 2008 14:15:44 +0200 haftmann tuned typedef interface
Mon, 29 Sep 2008 11:46:47 +0200 wenzelm handle _ should be avoided (spurious Interrupt will spoil the game);
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Thu, 12 Jun 2008 23:12:54 +0200 wenzelm use regular error function;
less more (0) -50 -30 tip