src/HOL/Import/proof_kernel.ML
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Mon, 03 May 2010 16:26:47 +0200 wenzelm minor tuning of Thm.strip_shyps -- no longer pervasive;
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;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Sat, 27 Mar 2010 21:38:38 +0100 wenzelm Typedef.info: separate global and local part, only the latter is transformed by morphisms;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Fri, 19 Mar 2010 00:47:23 +0100 wenzelm typedef etc.: no constraints;
Sat, 13 Mar 2010 14:43:04 +0100 wenzelm global typedef;
Fri, 26 Feb 2010 23:05:47 +0100 wenzelm use simplified Syntax.escape;
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;
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
less more (0) -100 -15 tip