src/Pure/thm.ML
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;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 added simple_fact; generalized no_attributes;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-08-01 wenzelm 2005-08-01 Compress.term;
2005-07-28 wenzelm 2005-07-28 added weaken, adjust_maxidx_thm;
2005-07-19 wenzelm 2005-07-19 tuned instantiate (avoid subst_atomic, subst_atomic_types); Logic.incr_tvar;