src/Pure/Proof/reconstruct.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-16 wenzelm 2009-07-16 incr_indexes (from Proofterm);
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 wenzelm 2009-07-02 added pro-forma proof constructor Inclass;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-01-27 wenzelm 2009-01-27 proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-30 wenzelm 2008-12-30 canonical Term.add_var_names, Term.add_tvar_namesT;
2008-11-16 berghofe 2008-11-16 - Corrected order of quantification over Frees. - Fixed bug in handling of TFrees that caused variable order to get mixed up.
2008-11-15 wenzelm 2008-11-15 adapted PThm;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-10-30 berghofe 2007-10-30 Handle Subscript exception when looking up bound variables.
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-10-31 haftmann 2006-10-31 fixed type signature of Type.varify
2006-09-21 wenzelm 2006-09-21 member (op =); tuned;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-02 wenzelm 2006-08-02 tuned;
2006-06-11 wenzelm 2006-06-11 avoid unqualified exception;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-13 wenzelm 2006-04-13 ignore sorts of consts declarations;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-07-15 wenzelm 2005-07-15 tuned;
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-05 wenzelm 2004-06-05 pretty_thm/goals_aux, pretty_flexpair: pp;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2002-11-27 berghofe 2002-11-27 prop_of now returns proposition in beta-eta normal form.
2002-11-13 berghofe 2002-11-13 Improved function decompose.
2002-10-21 berghofe 2002-10-21 - reconstruct_proof no longer relies on TypeInfer.infer_types - fixed problem with theorems containing TFrees
2002-09-30 berghofe 2002-09-30 Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
2002-07-10 berghofe 2002-07-10 expand_proof now also takes an optional term describing the proposition of the theorem to be expanded (to avoid problems with different theorems having the same names).
2002-06-28 berghofe 2002-06-28 Added function prop_of' taking assumption context as an argument.
2002-05-11 berghofe 2002-05-11 - Tuned function mk_cnstrts - Added function prop_of
2002-02-06 berghofe 2002-02-06 Indexes of variables in expanded proofs are now incremented to avoid clashes.
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-11-19 berghofe 2001-11-19 Moved fastype to Envir.