src/Pure/Proof/reconstruct.ML
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
Thu, 03 Jun 2010 23:56:05 +0200 wenzelm do not open Proofterm, which is very ould style;
Wed, 02 Jun 2010 21:39:35 +0200 wenzelm always unconstrain thm proofs;
Tue, 01 Jun 2010 10:48:38 +0200 berghofe Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.
Tue, 04 May 2010 12:30:15 +0200 wenzelm simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
Tue, 30 Mar 2010 15:25:30 +0200 krauss switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
Tue, 27 Oct 2009 22:56:14 +0100 wenzelm eliminated some old folds;
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
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, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 25 Jul 2009 10:31:27 +0200 wenzelm renamed structure Display_Goal to Goal_Display;
Thu, 23 Jul 2009 16:52:16 +0200 wenzelm clarified pretty_goals, pretty_thm_aux: plain context;
Mon, 20 Jul 2009 21:20:09 +0200 wenzelm moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Thu, 16 Jul 2009 23:12:12 +0200 wenzelm incr_indexes (from Proofterm);
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
Thu, 02 Jul 2009 20:55:44 +0200 wenzelm added pro-forma proof constructor Inclass;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Fri, 27 Feb 2009 16:38:52 +0100 wenzelm eliminated NJ's List.nth;
Tue, 27 Jan 2009 00:29:37 +0100 wenzelm proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
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;
Tue, 30 Dec 2008 21:47:11 +0100 wenzelm canonical Term.add_var_names, Term.add_tvar_namesT;
Sun, 16 Nov 2008 18:19:27 +0100 berghofe - Corrected order of quantification over Frees.
Sat, 15 Nov 2008 21:31:32 +0100 wenzelm adapted PThm;
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Wed, 19 Mar 2008 07:20:32 +0100 haftmann Type.lookup now curried
Tue, 30 Oct 2007 17:58:03 +0100 berghofe Handle Subscript exception when looking up bound variables.
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Tue, 31 Oct 2006 09:29:06 +0100 haftmann fixed type signature of Type.varify
Thu, 21 Sep 2006 19:05:56 +0200 wenzelm member (op =);
Fri, 15 Sep 2006 22:56:13 +0200 wenzelm renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
Wed, 02 Aug 2006 22:27:06 +0200 wenzelm tuned;
Sun, 11 Jun 2006 21:59:17 +0200 wenzelm avoid unqualified exception;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Wed, 26 Apr 2006 22:38:05 +0200 wenzelm tuned;
Thu, 13 Apr 2006 12:00:56 +0200 wenzelm ignore sorts of consts declarations;
Tue, 21 Mar 2006 12:18:15 +0100 wenzelm avoid polymorphic equality;
Mon, 06 Feb 2006 20:58:54 +0100 wenzelm Envir.(beta_)eta_contract;
Wed, 16 Nov 2005 17:45:30 +0100 wenzelm tuned Pattern.match/unify;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Fri, 02 Sep 2005 15:54:47 +0200 haftmann some 'assoc' etc. refactoring
Thu, 01 Sep 2005 22:15:12 +0200 wenzelm curried_lookup/update;
Mon, 01 Aug 2005 19:20:37 +0200 wenzelm replaced atless by term_ord;
Thu, 28 Jul 2005 15:19:49 +0200 wenzelm Sign.typ_unify;
Tue, 19 Jul 2005 17:21:47 +0200 wenzelm Logic.incr_tvar;
Fri, 15 Jul 2005 15:44:17 +0200 wenzelm tuned;
Wed, 13 Jul 2005 11:16:34 +0200 haftmann (intermediate commit)
Thu, 21 Apr 2005 19:13:03 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 05 Jun 2004 13:08:53 +0200 wenzelm pretty_thm/goals_aux, pretty_flexpair: pp;
Tue, 01 Jun 2004 12:33:50 +0200 wenzelm removed obsolete sort 'logic';
less more (0) -60 tip