src/Pure/thm.ML
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
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-15 wenzelm 2009-11-15 tuned;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
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 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;