src/HOL/simpdata.ML
changeset 6915 4ab8e31a8421
parent 6514 381fb2b084a4
child 6968 7f2977e96a5c
     1.1 --- a/src/HOL/simpdata.ML	Thu Jul 08 13:37:40 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jul 08 13:38:41 1999 +0200
     1.3 @@ -483,8 +483,7 @@
     1.4  
     1.5  (* install implicit simpset *)
     1.6  
     1.7 -simpset_ref() := HOL_ss;
     1.8 -
     1.9 +simpset_ref() := HOL_ss addcongs [if_weak_cong];
    1.10  
    1.11  
    1.12  (*** integration of simplifier with classical reasoner ***)