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;
2008-09-25 wenzelm 2008-09-25 explicit type OrdList.T;
2008-09-23 wenzelm 2008-09-23 added dest_deriv, removed external type deriv; misc tuning of internal deriv; more substantial promise/fulfill; promise_ord: reverse order on serial numbers; removed unused is_named; get_name: unfinished proof term;
2008-09-22 wenzelm 2008-09-22 type thm: fully internal derivation, no longer exported; incorporate former deriv.ML as internal abstract type; added rudimentary promise interface; tuned; added is_named (does not require finished derivation);
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-18 wenzelm 2008-09-18 added deriv.ML: Abstract derivations based on raw proof terms.
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies; Term.all;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-07 berghofe 2008-05-07 eq_assumption now uses aeconv instead of aconv.
2008-04-15 wenzelm 2008-04-15 Theory.eq_thy;
2008-04-13 wenzelm 2008-04-13 simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;
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-01-21 berghofe 2008-01-21 Removed Logic.auto_rename.
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;