src/Pure/thm.ML
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;
2005-07-14 wenzelm 2005-07-14 invoke_oracle: do not keep theory value, but theory_ref;
2005-07-06 wenzelm 2005-07-06 added full_prop_of: includes tpairs;
2005-07-06 wenzelm 2005-07-06 tuned maxidx;
2005-07-04 wenzelm 2005-07-04 dest_ctyp: raise exception for non-constructor; dest_comb: replaced expensive fastype_of by Term.argument_type; dest_abs: replaced expensive variant_abs by Term.dest_abs; hyps: fast_term_ord;
2005-07-01 wenzelm 2005-07-01 ctyp: added 'sorts' field; may_insert_typ/term/env_sorts: observe Sign.all_sorts_nonempty; may_insert_env_sorts: insert sorts of type subst only; instantiate: insert sorts of insts; tuned;
2005-06-29 wenzelm 2005-06-29 more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
2005-06-09 wenzelm 2005-06-09 axioms: NameSpace.table;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
2005-05-31 wenzelm 2005-05-31 added eq_thms;
2005-05-22 wenzelm 2005-05-22 tuned terms_of_tpairs;
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-07 wenzelm 2005-04-07 added get_axiom_i, invoke_oracle_i;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 paulson 2005-01-24 thin_tac now works on P==>Q
2004-10-26 berghofe 2004-10-26 Changed function cabs to also allow abstraction over Vars.
2004-07-29 berghofe 2004-07-29 - optimized nodup_vars check in capply - new function dest_ctyp
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 adapted names of some sort ops;
2002-10-21 berghofe 2002-10-21 Changed handling of flex-flex constraints: now stored in separate tpairs field of theorem record.
2002-10-10 nipkow 2002-10-10 added failure trace information to pattern unification
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2002-08-27 wenzelm 2002-08-27 added proof_of;
2002-02-28 wenzelm 2002-02-28 moved match_bvs, match_bvars, renAbs to term.ML;
2002-02-21 wenzelm 2002-02-21 fixed get_name_tags in order to work with hyps;
2002-01-17 wenzelm 2002-01-17 added prop_of: thm -> term (at last!);
2001-12-14 wenzelm 2001-12-14 varifyT' returns newly introduces variables;
2001-10-04 wenzelm 2001-10-04 major_prem_of: Logic.strip_assums_concl;
2001-09-28 berghofe 2001-09-28 Exchanged % and %%.
2001-09-13 berghofe 2001-09-13 Fixed proof term bug in permute_prems.