src/Pure/thm.ML
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.
2001-08-31 berghofe 2001-08-31 Replaced old derivations by proof terms.
2001-01-03 wenzelm 2001-01-03 Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-11-17 wenzelm 2000-11-17 Envir.beta_norm;
2000-11-07 berghofe 2000-11-07 - Moved rewriting functions to meta_simplifier.ML - dest_abs now also takes an optional variable name as an argument - beta_conversion takes additional flag as an argument. Fully reduces the term if set to true Some tuning: - tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive, transitive, beta_conversion, abstract_rule - combination: chktypes derives types of f and t from type of == instead of using fastype_of New primitives: - eta_conversion - incr_indexes: increment indexes in theorems - cterm_incr_indexes: increment indexes in cterms - cterm_match, cterm_first_order_match - rename_boundvars
2000-10-27 wenzelm 2000-10-27 back to 1.167, due to Emacs/CVS casualty!!;
2000-10-27 wenzelm 2000-10-27 *** empty log message ***
2000-09-07 nipkow 2000-09-07 Added meaningful output to cong-error msg.
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-16 nipkow 2000-08-16 Fixed completeness bug in simplifier: congruence rules could preclude rewrites of the partially applied constant.
2000-08-02 wenzelm 2000-08-02 derivations: maintain oracle flag;
2000-07-30 wenzelm 2000-07-30 added sign_of_cterm;
2000-06-03 wenzelm 2000-06-03 fixed Thm.eq_thm: use Sign.joinable;
2000-05-10 wenzelm 2000-05-10 dest_mss: sort procs wrt. names;
2000-05-08 wenzelm 2000-05-08 tuned msg;
2000-03-30 wenzelm 2000-03-30 read_def_cterms: use Sign.read_def_terms;
2000-03-10 berghofe 2000-03-10 Envir now uses Vartab instead of association lists.
2000-02-27 wenzelm 2000-02-27 added major_prem_of;
2000-02-24 wenzelm 2000-02-24 tuned;
2000-02-24 wenzelm 2000-02-24 capply, cabs: Sign.nodup_vars;
2000-01-17 paulson 2000-01-17 Thm.instantiate no longer normalizes, but Drule.instantiate does
1999-12-16 paulson 1999-12-16 SOUNDNESS BUG FIX for rotate_rule. The original code did not expect nested parameters such as !!y. Goal "!!x. x = a ==> (!!y. y ~= a ==> False)"; by (rotate_tac 1 1); be notE 1; ba 1; qed "foo"; val FalseI = standard (True_not_False RS (standard (refl RS foo)));
1999-10-22 wenzelm 1999-10-22 debug_simp;