src/Pure/thm.ML
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;
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list
2006-08-03 wenzelm 2006-08-03 tuned;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-30 wenzelm 2006-07-30 adjust_maxidx: pass explicit lower bound; tuned interfaces;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 tuned exception handling;
2006-07-04 wenzelm 2006-07-04 varifyT: no longer pervasive;
2006-06-17 wenzelm 2006-06-17 added generalize rule; added maxidx_thm;
2006-06-13 wenzelm 2006-06-13 added hyps_of; tuned;
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-05-01 wenzelm 2006-05-01 class_triv: Sign.certify_class;
2006-04-29 wenzelm 2006-04-29 added unconstrainT;
2006-04-26 wenzelm 2006-04-26 curried Seq.cons;
2006-04-13 wenzelm 2006-04-13 added maxidx_of;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-10 mengj 2006-03-10 Shortened the exception messages from assume.
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-07 wenzelm 2006-02-07 removed obsolete sign_of_cterm; adapted Sign.certify_term;
2006-02-06 wenzelm 2006-02-06 union_tpairs: Library.merge; Envir.(beta_)eta_contract; tuned;
2006-01-21 wenzelm 2006-01-21 simplified type attribute; added rule/declaration_attribute (from drule.ML); added theory/proof_attributes; removed apply(s)_attributes;
2005-12-23 wenzelm 2005-12-23 turned bicompose_no_flatten into compose_no_flatten, without elimination;
2005-12-22 wenzelm 2005-12-22 added bicompose_no_flatten, which refrains from changing the shape of the new subgoals;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-09 wenzelm 2005-11-09 Thm.varifyT': natural argument order;
2005-10-28 wenzelm 2005-10-28 added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;
2005-10-15 wenzelm 2005-10-15 tuned comment;
2005-09-29 wenzelm 2005-09-29 abstract_rule: tuned exception msgs;