src/Pure/proofterm.ML
2010-06-02 wenzelm 2010-06-02 always unconstrain thm proofs;
2010-06-02 wenzelm 2010-06-02 normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 - outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-14 wenzelm 2010-05-14 added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-13 wenzelm 2010-05-13 conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13 wenzelm 2010-05-13 avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13 wenzelm 2010-05-13 raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13 wenzelm 2010-05-13 unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13 wenzelm 2010-05-13 added Proofterm.get_name variants according to krauss/schropp; tuned signature;
2010-05-08 wenzelm 2010-05-08 tuned signature;
2010-05-08 wenzelm 2010-05-08 added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
2010-05-07 wenzelm 2010-05-07 strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-04 wenzelm 2010-05-04 proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
2010-05-04 wenzelm 2010-05-04 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04 wenzelm 2010-05-04 renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-03-21 wenzelm 2010-03-21 do not open ML structures;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-16 wenzelm 2009-11-16 generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-05 wenzelm 2009-11-05 revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
2009-11-04 wenzelm 2009-11-04 fulfill_proof_future: tuned important special case of singleton promise;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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;