src/Pure/thm.ML
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;
2007-08-17 wenzelm 2007-08-17 compress: proper check_thy;
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref; thread-safeness: when creating certified items, perform Theory.check_thy *last*;
2007-07-11 berghofe 2007-07-11 Added function norm_proof for normalizing the proof term corresponding to a theorem.
2007-07-08 wenzelm 2007-07-08 thm tag: Markup.property list;
2007-07-05 wenzelm 2007-07-05 added type conv; merge_thys: removed dead exception handlers; tuned;
2007-06-25 wenzelm 2007-06-25 added eta_long_conversion;
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-10 wenzelm 2007-05-10 added dest_fun/fun2/arg1; removed dest_binop; renamed cterm_(fo_)match to (fo_)match; renamed cterm_incr_indexes to incr_indexes_cterm;
2007-04-14 wenzelm 2007-04-14 removed obsolete read_ctyp, read_def_cterm; moved read_def_cterms, read_cterm to more_thm.ML; avoid rep_theory;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;