src/Pure/thm.ML
1997-03-14 nipkow 1997-03-14 Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
1997-02-21 paulson 1997-02-21 Introduction of rotate_rule
1997-02-15 oheimb 1997-02-15 added del_congs
1997-02-14 nipkow 1997-02-14 Made troublesome simplifier warning dependent on trace_simp.
1997-01-22 nipkow 1997-01-22 Added warning msg when the simplifier cannot use a premise as a rewrite rule because it contains (type) unknowns.
1997-01-16 wenzelm 1997-01-16 added termless parameter; added simplification procedures;
1996-12-13 wenzelm 1996-12-13 fixed warning;
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-12 paulson 1996-11-12 Changed some mem, ins and union calls to be monomorphic
1996-11-06 wenzelm 1996-11-06 tuned fix_shyps a little bit more;
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max nodup_Vars now updates maxidx
1996-10-30 paulson 1996-10-30 Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
1996-10-01 wenzelm 1996-10-01 added shyps comment;
1996-09-30 nipkow 1996-09-30 Inserted check for rewrite rules which introduce extra Vars on the rhs.
1996-06-28 paulson 1996-06-28 Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users
1996-06-14 paulson 1996-06-14 Now del_simp catches the right exception!
1996-04-30 clasohm 1996-04-30 moved dest_cimplies to drule.ML; added adjust_maxidx
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-03 nipkow 1996-04-03 Plugged some more loopholes with nodup_Vars.
1996-03-21 paulson 1996-03-21 name_thm no longer takes a theory argument, as the name no longer hides the previous derivation. Deleted sign_of_thm as redundant.
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-03-11 nipkow 1996-03-11 Non-matching congruence rule in rewriter is simply ignored. Used to cause error message.
1996-03-11 paulson 1996-03-11 name_thm: now keeps the previous deriviation!
1996-03-05 paulson 1996-03-05 Addition of oracles
1996-03-01 paulson 1996-03-01 Addition of proof objects
1996-02-22 clasohm 1996-02-22 added cabs and crep_thm
1996-02-22 clasohm 1996-02-22 removed mk_prop; added capply; simplified dest_abs
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-13 nipkow 1996-02-13 Added check for duplicate vars with distinct types/sorts (nodup_Vars)
1996-02-13 clasohm 1996-02-13 added dest_comb, dest_abs and mk_prop for manipulating cterms
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-22 paulson 1995-12-22 Commented the datatype declaration of thm. Declared compress: thm -> thm to copy a thm and maximize sharing in it. "ext_axms" now calls Term.compress_term so that stored axioms use sharing.
1995-12-08 paulson 1995-12-08 New function read_cterms is a combination of read_def_cterm and read_cterm. It reads and simultaneously type-checks a list of strings. cterm_of no longer catches exception TYPE; instead it must be caught later on and a message printed using Sign.exn_type_msg. More informative messages can be printed this way.
1995-09-21 wenzelm 1995-09-21 bicompose_aux: tuned fix_shyps; simplifier: fixed handling of shyps;
1995-09-01 wenzelm 1995-09-01 considerably tuned shyps handling;
1995-08-17 nipkow 1995-08-17 deactivated fix_shyps.
1995-08-01 wenzelm 1995-08-01 MAJOR changes: added shyps component to type thm; added rules strip_shyps, implies_intr_shyps; fixed rules to handle shyps properly;
1995-07-25 lcp 1995-07-25 match_bvs no longer puts a name in the alist if it is null ("")
1995-06-26 wenzelm 1995-06-26 added add_trrules_i; cleaned up signature THM; improved some comments;
1995-04-16 nipkow 1995-04-16 Fixed old bug in the simplifier. Term to be simplified now carries around its maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1 in most cases (ie no Vars), hence reasonable overhead.
1995-04-11 nipkow 1995-04-11 Added comment to function "loops".
1995-04-10 nipkow 1995-04-10 Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that the maxidx-filed of thms is computed correctly.
1995-03-30 nipkow 1995-03-30 Simplification: used Logic.occs instead of mem add_term_frees
1995-03-15 clasohm 1995-03-15 removed print_msg parameter of infer_types
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-16 nipkow 1995-02-16 Improved test for looping rewrite rules.
1995-02-08 nipkow 1995-02-08 Improved check for looping conditional rewrite rules.
1994-12-09 wenzelm 1994-12-09 improved axioms_of: returns thms as the manual says;
1994-11-21 lcp 1994-11-21 Pure/thm/norm_term_skip: new, for skipping normalization of the context Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in new subgoals) and avoids normalizing the first nlift assumptions in the case where the proof state is not affected. Pure/thm/norm_term_skip: now normalizes types of parameters Pure/thm/THM: aligned colons
1994-11-02 nipkow 1994-11-02 Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
1994-10-28 nipkow 1994-10-28 Prepared the code for preservation of bound var names during rewriting. Still requires a matching function for HO-patterns.
1994-10-04 clasohm 1994-10-04 added print_msg; added call of Type.infer_types to resolve ambiguities
1994-09-27 nipkow 1994-09-27 Modified termord to take account of the Abs-Abs case.
1994-08-23 wenzelm 1994-08-23 read_def_cterm: minor changes; merge_thm_sgs: improved error msg;
1994-08-19 wenzelm 1994-08-19 added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;