src/Pure/thm.ML
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 bindings;
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-28 wenzelm 2009-09-28 tuned internal source structure;
2009-09-16 wenzelm 2009-09-16 replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
2009-07-26 wenzelm 2009-07-26 lambda/cabs/all: named variants;
2009-07-21 wenzelm 2009-07-21 simultaneous join_proofs; removed obsolete promises_of;
2009-07-21 wenzelm 2009-07-21 prefer simultaneous join -- for improved scheduling;
2009-07-19 wenzelm 2009-07-19 support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies); export promises_of; removed obsolete pending_groups; tuned;
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-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-06 wenzelm 2009-07-06 clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-07-06 wenzelm 2009-07-06 clarified Thm.of_class/of_sort/class_triv;
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 strip_shyps: remove top sort, which is logically insignificant;
2009-07-02 wenzelm 2009-07-02 added pro-forma proof constructor Inclass;
2009-03-25 wenzelm 2009-03-25 fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete); more explicit oracle_proof;
2009-03-24 wenzelm 2009-03-24 status_of: need to include local promises as well!
2009-03-24 wenzelm 2009-03-24 display derivation status of thms;
2009-03-17 wenzelm 2009-03-17 eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly; tuned;
2009-03-16 wenzelm 2009-03-16 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-07 wenzelm 2009-03-07 moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2009-01-27 wenzelm 2009-01-27 thm_proof: replaced lazy by composed futures;
2009-01-10 wenzelm 2009-01-10 future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10 wenzelm 2009-01-10 added pending_groups -- accumulates task groups of local derivations only;
2009-01-01 wenzelm 2009-01-01 avoid polymorphic equality;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
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-06 wenzelm 2008-12-06 renamed force_proof to join_proof;
2008-12-05 wenzelm 2008-12-05 refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises); name_thm: actually maintain max_promise/open_promises here (!), reduce open_promises as far as possible; tuned;
2008-12-05 haftmann 2008-12-05 merged
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-05 wenzelm 2008-12-05 merged
2008-12-04 wenzelm 2008-12-04 future proofs: pass actual futures to facilitate composite computations; removed join_futures -- superceded by higher-level PureThy.force_proofs;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-23 wenzelm 2008-11-23 future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
2008-11-18 wenzelm 2008-11-18 fulfill_proof/thm_proof: commuted lazyness; join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);
2008-11-18 wenzelm 2008-11-18 added force_proofs; join_futures: no errors here;
2008-11-17 wenzelm 2008-11-17 tuned promise/fullfill;
2008-11-16 wenzelm 2008-11-16 put_name/thm_proof: promises are filled with fulfilled proofs; tuned;
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;
2008-10-23 wenzelm 2008-10-23 renamed get_axiom_i to axiom, removed obsolete get_axiom; reduced pervasive names;
2008-10-21 wenzelm 2008-10-21 join results in isolation;
2008-10-16 wenzelm 2008-10-16 added weaken_sorts; strip_shyps: minimal list of minimized extra sorts; tuned;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-10-01 wenzelm 2008-10-01 more precise join_futures, improved termination;
2008-09-30 wenzelm 2008-09-30 export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;
2008-09-28 wenzelm 2008-09-28 join earlier promises first;
2008-09-28 wenzelm 2008-09-28 promise_result: enforce strictly sequential dependencies, via serial numbers;
2008-09-27 wenzelm 2008-09-27 Future.release_results;
2008-09-27 wenzelm 2008-09-27 promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;
2008-09-25 wenzelm 2008-09-25 simplified promise; fulfill is internal only; more robust join_futures;
2008-09-25 wenzelm 2008-09-25 abtract types: plain datatype with opaque signature matching; promise: join pending futures at end of theory;