src/HOL/simpdata.ML
changeset 4744 4469d498cd48
parent 4743 b3bfcbd9fb93
child 4769 bb60149fe21b
     1.1 --- a/src/HOL/simpdata.ML	Thu Mar 12 13:17:13 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 13 18:15:14 1998 +0100
     1.3 @@ -400,8 +400,7 @@
     1.4  			    setSSolver   safe_solver
     1.5  			    setSolver  unsafe_solver
     1.6  			    setmksimps (mksimps mksimps_pairs)
     1.7 -			    setmkeqTrue mk_meta_eq_True
     1.8 -                            addsplits [expand_if];
     1.9 +			    setmkeqTrue mk_meta_eq_True;
    1.10  
    1.11  val HOL_ss = 
    1.12      HOL_basic_ss addsimps 
    1.13 @@ -413,7 +412,8 @@
    1.14         disj_not1, not_all, not_ex, cases_simp]
    1.15       @ ex_simps @ all_simps @ simp_thms)
    1.16       addsimprocs [defALL_regroup,defEX_regroup]
    1.17 -     addcongs [imp_cong];
    1.18 +     addcongs [imp_cong]
    1.19 +     addsplits [expand_if];
    1.20  
    1.21  qed_goal "if_distrib" HOL.thy
    1.22    "f(if c then x else y) = (if c then f x else f y)"