src/Pure/thm.ML
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;
2007-02-26 wenzelm 2007-02-26 moved some non-kernel material to more_thm.ML;
2007-02-04 wenzelm 2007-02-04 old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
2007-01-02 wenzelm 2007-01-02 Term.lambda: abstract over arbitrary closed terms;
2006-12-12 wenzelm 2006-12-12 tuned error messages;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-29 wenzelm 2006-11-29 simplified Logic.count_prems;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-11-05 wenzelm 2006-11-05 removed obsolete first_duplicate;
2006-10-31 haftmann 2006-10-31 fixed type signature of Type.varify
2006-10-11 haftmann 2006-10-11 abandoned findrep
2006-10-07 wenzelm 2006-10-07 added def_name_optional;
2006-10-01 wenzelm 2006-10-01 cterm_match: avoid recalculation of maxidx;
2006-09-21 wenzelm 2006-09-21 added dest_binop;
2006-09-18 wenzelm 2006-09-18 added dest_arg, i.e. a tuned version of #2 o dest_comb;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15 wenzelm 2006-09-15 instantiate: omit has_duplicates check, which is irrelevant for soundness;
2006-09-12 wenzelm 2006-09-12 ctyp: maintain maxidx; cterm_match: tight maxidx for substitution; instantiate: determine maxidx from insts -- major performance improvement; moved term subst functions to TermSubst; tuned;