src/Pure/proofterm.ML
2006-10-04 haftmann 2006-10-04 *** empty log message ***
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-12 wenzelm 2006-09-12 moved term subst functions to TermSubst;
2006-08-02 wenzelm 2006-08-02 replaced maxidx_of_proof by maxidx_proof;
2006-07-19 wenzelm 2006-07-19 tuned;
2006-07-18 wenzelm 2006-07-18 fold_proof_terms: canonical arguments; removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-04 wenzelm 2006-07-04 added map_proof_terms_option; tuned generalize, instantiate;
2006-06-17 wenzelm 2006-06-17 added generalize rule;
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-07 berghofe 2006-04-07 Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.
2006-03-21 wenzelm 2006-03-21 remove (op =); tuned;
2006-03-08 wenzelm 2006-03-08 infer_derivs: avoid allocating empty MinProof;
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2005-12-22 wenzelm 2005-12-22 bicompose_proof: no_flatten;
2005-12-01 berghofe 2005-12-01 Improved norm_proof to handle proofs containing term (type) variables with same name but different types (sorts): Offending term (type) variables are replaced by dummy (T)Frees before applying the substitution.
2005-10-28 wenzelm 2005-10-28 Logic.lift_all;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-19 wenzelm 2005-09-19 shrink: compress terms and types; prefer member/insert over polymorphic mem/ins;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-03 berghofe 2005-08-03 - Tuned handling of oracles - Put arguments of axms_of_proof and thms_of_proof into "canonical order"
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-07-28 wenzelm 2005-07-28 adapted Type.typ_match; tuned;
2005-07-19 wenzelm 2005-07-19 tuned instantiate interface; Logic.incr_tvar;
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-06-22 wenzelm 2005-06-22 renamed init to init_data;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-03-26 gagern 2005-03-26 op vor infix-Konstruktoren im datatype binding zum besseren Parsen
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-07-09 berghofe 2004-07-09 - Expressed infer_derivs' in terms of infer_deriv - Eta-expanded function instantiate to delay evaluation (avoids inefficiencies when proof terms are switched off)
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-21 wenzelm 2004-05-21 adapted tsig interface;
2002-12-13 berghofe 2002-12-13 size_of_proof no longer includes size_of_term
2002-12-10 berghofe 2002-12-10 Added size_of_proof.
2002-10-21 berghofe 2002-10-21 Removed Logic.strip_flexpairs.
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2002-08-27 wenzelm 2002-08-27 thms/axms_of_proof: proper handling of MinProof;
2002-05-04 berghofe 2002-05-04 Added skeletons to speed up rewriting on proof terms.
2002-02-21 wenzelm 2002-02-21 fixed get_name_tags in order to work with hyps;
2002-02-20 berghofe 2002-02-20 New function change_type for changing type assignments of theorems, axioms and oracles.
2002-02-14 wenzelm 2002-02-14 made MLWorks happy;
2002-02-06 berghofe 2002-02-06 Added function could_unify to speed up rewriting of proof terms.
2002-02-05 berghofe 2002-02-05 New function maxidx_of_proof.
2001-12-14 wenzelm 2001-12-14 type_env;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-24 wenzelm 2001-11-24 fixed SML/NJ error (!?);
2001-11-24 wenzelm 2001-11-24 use merge_lists, merge_alists;
2001-11-24 berghofe 2001-11-24 Extended match_proof to handle abstractions.
2001-11-19 berghofe 2001-11-19 - Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data
2001-11-09 wenzelm 2001-11-09 theory data: finish method;