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