src/Pure/proofterm.ML
2010-05-07 ago strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-04 ago proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04 ago simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04 ago renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-03-21 ago do not open ML structures;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 ago modernized structure Term_Ord;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-16 ago generalized procs for rewrite_proof: allow skeleton;
2009-11-08 ago adapted Theory_Data;
2009-11-05 ago revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
2009-11-04 ago fulfill_proof_future: tuned important special case of singleton promise;
2009-10-29 ago standardized filter/filter_out;
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-01 ago back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
2009-09-30 ago eliminated redundant parameters;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-28 ago fold_body_thms: pass pthm identifier;
2009-09-27 ago fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
2009-07-24 ago get_name: cover only PThm, not PAxm;
2009-07-21 ago prefer simultaneous join -- for improved scheduling;
2009-07-19 ago tuned;
2009-07-18 ago added join_bodies;
2009-07-18 ago tuned prf_subst: use structure Same;
2009-07-17 ago tuned/modernized Envir.subst_XXX;
2009-07-17 ago tuned/modernized Envir operations;
2009-07-16 ago tuned incr_indexes;
2009-07-16 ago tuned map_proof_terms_option;
2009-07-16 ago use structure Same;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 ago added pro-forma proof constructor Inclass;
2009-03-25 ago removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
2009-03-24 ago status_of: simultaneous list;
2009-03-24 ago display derivation status of thms;
2009-02-27 ago eliminated NJ's List.nth;
2009-01-27 ago thm_proof: recovered single-threaded version;
2009-01-27 ago thm_proof: replaced lazy by composed futures;
2009-01-27 ago proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-30 ago freeze_thaw: canonical Term.add_XXX operations;
2008-12-04 ago renamed type Lazy.T to lazy;
2008-11-23 ago tuned;
2008-11-23 ago eliminated finish_proof, keep pre/post normalization of results separate;
2008-11-18 ago fulfill_proof/thm_proof: commuted lazyness;
2008-11-17 ago finish_proof: undefined promises may occur here;
2008-11-17 ago unified treatment of PAxm/Oracle/Promise in basic proof term operations;
2008-11-16 ago proof_body/pthm: removed redundant types field;
2008-11-16 ago Frees in PThms are now quantified in the order of their appearance in the
2008-11-15 ago reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
2008-09-23 ago added conditional add_oracles, keep oracles_of_proof private;
2008-09-22 ago added Promise constructor, which is similar to Oracle but may be replaced later;
2008-06-23 ago Logic.all/mk_equals/mk_implies;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago eliminated theory ProtoPure;