src/Pure/proofterm.ML
2009-10-01 wenzelm 2009-10-01 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 wenzelm 2009-09-30 eliminated redundant parameters;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;
2009-09-27 wenzelm 2009-09-27 fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
2009-07-24 wenzelm 2009-07-24 get_name: cover only PThm, not PAxm;
2009-07-21 wenzelm 2009-07-21 prefer simultaneous join -- for improved scheduling;
2009-07-19 wenzelm 2009-07-19 tuned;
2009-07-18 wenzelm 2009-07-18 added join_bodies;
2009-07-18 wenzelm 2009-07-18 tuned prf_subst: use structure Same;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-16 wenzelm 2009-07-16 tuned incr_indexes;
2009-07-16 wenzelm 2009-07-16 tuned map_proof_terms_option; eliminated apsome, apsome'; tuned;
2009-07-16 wenzelm 2009-07-16 use structure Same; do not open Envir;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 wenzelm 2009-07-02 added pro-forma proof constructor Inclass;
2009-03-25 wenzelm 2009-03-25 removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof; added approximate_proof_body -- replaces former make_proof_body; added all_oracles_of; oracle_proof: explicit oracle result; fulfill_proof/thm_proof: require proper proof_body futures, to maintain full account of oracles and thms (repairs a serious problem of the old version);
2009-03-24 wenzelm 2009-03-24 status_of: simultaneous list;
2009-03-24 wenzelm 2009-03-24 display derivation status of thms;
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;