src/Pure/thm.ML
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;
1999-09-29 wenzelm 1999-09-29 removed implies_intr_shyps; removed force_strip_shyps (at last!); strip_shyps: proper witness_sorts; fix_shyps: tuned for all_sorts_nonempty;
1999-09-09 wenzelm 1999-09-09 added no_prems;
1999-09-09 wenzelm 1999-09-09 removed obsolete comment;
1999-08-23 nipkow 1999-08-23 Now rewrite rules with flexible heads are allowed.
1999-08-23 nipkow 1999-08-23 Corrected two busg in the simplifier.
1999-08-18 wenzelm 1999-08-18 (*no fix_shyps*);
1999-08-18 paulson 1999-08-18 new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-23 wenzelm 1999-07-23 tuned add_term_varnames;
1999-07-08 wenzelm 1999-07-08 improved error msgs of instantiate;
1999-07-06 wenzelm 1999-07-06 added clear_mss;
1999-06-05 wenzelm 1999-06-05 varifyT': observe additional 'fixed' tfrees;
1999-04-29 nipkow 1999-04-29 Eta contraction is now performed all the time during rewriting.
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-03-17 wenzelm 1999-03-17 added def_name; class_triv: Sign.sg;
1999-01-12 wenzelm 1999-01-12 signature BASIC_THM; theorem / axiom deriv: added tags; get/put_name_tags; type attribute;
1998-10-08 nipkow 1998-10-08 Further improvement of the simplifier.
1998-10-07 nipkow 1998-10-07 Tuned simplifier not to re-normalized already normalized terms.
1998-09-18 paulson 1998-09-18 improved error messages
1998-08-19 wenzelm 1998-08-19 assume: adjust_maxidx;
1998-08-19 paulson 1998-08-19 The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.
1998-06-05 wenzelm 1998-06-05 Object.T;
1998-04-29 wenzelm 1998-04-29 tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;
1998-04-22 nipkow 1998-04-22 Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.
1998-04-04 wenzelm 1998-04-04 tuned trace msgs;
1998-03-12 nipkow 1998-03-12 Made mutual simplification of prems a special case.