src/Pure/proofterm.ML
2007-07-11 ago Added function rew_proof (for pre-normalizing proofs).
2007-06-08 ago Adapted Proofterm.bicompose_proof to Larry's changes in
2007-05-31 ago simplified/unified list fold;
2007-05-07 ago simplified DataFun interfaces;
2007-04-13 ago canonical merge operations
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-10-04 ago *** empty log message ***
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-12 ago moved term subst functions to TermSubst;
2006-08-02 ago replaced maxidx_of_proof by maxidx_proof;
2006-07-19 ago tuned;
2006-07-18 ago fold_proof_terms: canonical arguments;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-04 ago added map_proof_terms_option;
2006-06-17 ago added generalize rule;
2006-04-29 ago tuned;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-07 ago Added alternative version of thms_of_proof that does not recursively
2006-03-21 ago remove (op =);
2006-03-08 ago infer_derivs: avoid allocating empty MinProof;
2006-02-11 ago tuned;
2006-02-06 ago subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2005-12-22 ago bicompose_proof: no_flatten;
2005-12-01 ago Improved norm_proof to handle proofs containing term (type) variables
2005-10-28 ago Logic.lift_all;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-19 ago shrink: compress terms and types;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-12 ago introduced new-style AList operations
2005-09-08 ago introduces some modern-style AList operations
2005-09-01 ago curried_lookup/update;
2005-08-31 ago refer to theory instead of low-level tsig;
2005-08-03 ago - Tuned handling of oracles
2005-08-01 ago replaced atless by term_ord;
2005-07-28 ago adapted Type.typ_match;
2005-07-19 ago tuned instantiate interface;
2005-07-13 ago (intermediate commit)
2005-06-22 ago renamed init to init_data;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-04-21 ago - Eliminated nodup_vars check.
2005-03-26 ago op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-07-09 ago - Expressed infer_derivs' in terms of infer_deriv
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-05-21 ago adapted tsig interface;
2002-12-13 ago size_of_proof no longer includes size_of_term
2002-12-10 ago Added size_of_proof.
2002-10-21 ago Removed Logic.strip_flexpairs.
2002-10-07 ago take/drop -> splitAt
2002-08-27 ago thms/axms_of_proof: proper handling of MinProof;
2002-05-04 ago Added skeletons to speed up rewriting on proof terms.
2002-02-21 ago fixed get_name_tags in order to work with hyps;
2002-02-20 ago New function change_type for changing type assignments of theorems,
2002-02-14 ago made MLWorks happy;
2002-02-06 ago Added function could_unify to speed up rewriting of proof terms.
2002-02-05 ago New function maxidx_of_proof.
2001-12-14 ago type_env;