src/Pure/thm.ML
1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-23 paulson 1997-07-23 Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
1997-07-23 wenzelm 1997-07-23 improved simp tracing;
1997-07-22 wenzelm 1997-07-22 added dest_mss, merge_mss; fixed matching of simproc lhss;
1997-07-18 wenzelm 1997-07-18 tuned warning; improved comments;
1997-06-05 paulson 1997-06-05 freezeT now refers to Type.freeze_thaw
1997-04-25 wenzelm 1997-04-25 improved tmp comment;
1997-04-24 nipkow 1997-04-24 rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.
1997-04-23 wenzelm 1997-04-23 simprocs called with eta contracted subterm;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
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.