1.1 --- a/src/HOL/simpdata.ML	Wed Sep 18 18:19:43 2002 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 19 16:00:27 2002 +0200
     1.3 @@ -136,18 +136,18 @@
     1.4  
     1.5  (*Make meta-equalities.  The operator below is Trueprop*)
     1.6  
     1.7 -fun mk_meta_eq r = r RS eq_reflection;
     1.8 +fun mk_meta_eq r = r nRS eq_reflection;
     1.9  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    1.10  
    1.11  fun mk_eq th = case concl_of th of
    1.12          Const("==",_)$_$_       => th
    1.13      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    1.14 -    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    1.15 -    |   _                       => th RS Eq_TrueI;
    1.16 -(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.17 +    |   _$(Const("Not",_)$_)    => th nRS Eq_FalseI
    1.18 +    |   _                       => th nRS Eq_TrueI;
    1.19 +(* Expects Trueprop(.) if not == *)
    1.20  
    1.21  fun mk_eq_True r =
    1.22 -  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
    1.23 +  Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
    1.24  
    1.25  (*Congruence rules for = (instead of ==)*)
    1.26  fun mk_meta_cong rl =
    1.27 @@ -188,21 +188,15 @@
    1.28  val Addsplits        = Splitter.Addsplits;
    1.29  val Delsplits        = Splitter.Delsplits;
    1.30  
    1.31 -(*In general it seems wrong to add distributive laws by default: they
    1.32 -  might cause exponential blow-up.  But imp_disjL has been in for a while
    1.33 -  and cannot be removed without affecting existing proofs.  Moreover,
    1.34 -  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
    1.35 -  grounds that it allows simplification of R in the two cases.*)
    1.36 -
    1.37  val mksimps_pairs =
    1.38    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.39     ("All", [spec]), ("True", []), ("False", []),
    1.40     ("If", [if_bool_eq_conj RS iffD1])];
    1.41  
    1.42 -(* ###FIXME: move to Provers/simplifier.ML
    1.43 +(*
    1.44  val mk_atomize:      (string * thm list) list -> thm -> thm list
    1.45 +looks too specific to move it somewhere else
    1.46  *)
    1.47 -(* ###FIXME: move to Provers/simplifier.ML *)
    1.48  fun mk_atomize pairs =
    1.49    let fun atoms th =
    1.50          (case concl_of th of
    1.51 @@ -210,7 +204,7 @@
    1.52               (case head_of p of
    1.53                  Const(a,_) =>
    1.54                    (case assoc(pairs,a) of
    1.55 -                     Some(rls) => flat (map atoms ([th] RL rls))
    1.56 +                     Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
    1.57                     | None => [th])
    1.58                | _ => [th])
    1.59           | _ => [th])
    1.60 @@ -237,6 +231,12 @@
    1.61      setmkeqTrue mk_eq_True
    1.62      setmkcong mk_meta_cong;
    1.63  
    1.64 +(*In general it seems wrong to add distributive laws by default: they
    1.65 +  might cause exponential blow-up.  But imp_disjL has been in for a while
    1.66 +  and cannot be removed without affecting existing proofs.  Moreover,
    1.67 +  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
    1.68 +  grounds that it allows simplification of R in the two cases.*)
    1.69 +
    1.70  val HOL_ss =
    1.71      HOL_basic_ss addsimps
    1.72       ([triv_forall_equality, (* prunes params *)