src/Pure/proofterm.ML
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-01-27 wenzelm 2009-01-27 thm_proof: recovered single-threaded version;
2009-01-27 wenzelm 2009-01-27 thm_proof: replaced lazy by composed futures;
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 term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
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 freeze_thaw: canonical Term.add_XXX operations; varify: regular name context;
2008-12-04 wenzelm 2008-12-04 renamed type Lazy.T to lazy;
2008-11-23 wenzelm 2008-11-23 tuned;
2008-11-23 wenzelm 2008-11-23 eliminated finish_proof, keep pre/post normalization of results separate;
2008-11-18 wenzelm 2008-11-18 fulfill_proof/thm_proof: commuted lazyness;
2008-11-17 wenzelm 2008-11-17 finish_proof: undefined promises may occur here;
2008-11-17 wenzelm 2008-11-17 unified treatment of PAxm/Oracle/Promise in basic proof term operations; refined promise/fulfill: maintain proper type instantiation, disallow term variables; thm_proof: uniform finish_proof before and after fulfill;
2008-11-16 wenzelm 2008-11-16 proof_body/pthm: removed redundant types field; fold_proof_atoms: unified recursive case with fold_body_thms; tuned signature;
2008-11-16 berghofe 2008-11-16 Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.
2008-11-15 wenzelm 2008-11-15 reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;
2008-09-23 wenzelm 2008-09-23 added conditional add_oracles, keep oracles_of_proof private; added fulfill; removed unused is_named; tuned some table operations;
2008-09-22 wenzelm 2008-09-22 added Promise constructor, which is similar to Oracle but may be replaced later; added promise_proof; export min_proof, mk_min_proof; moved infer_derivs to thm.ML as derive_rule0/1/2; tuned oracles_of_proof; added is_named;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-07-11 berghofe 2007-07-11 Added function rew_proof (for pre-normalizing proofs).
2007-06-08 berghofe 2007-06-08 Adapted Proofterm.bicompose_proof to Larry's changes in Logic.assum_pairs from 2005-01-24 (revision 1.44).
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-13 haftmann 2007-04-13 canonical merge operations
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
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)