src/HOL/simpdata.ML
changeset 4677 c4b07b8579fd
parent 4669 06f3c56dcba8
child 4681 a331c1f5a23e
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 03 15:15:04 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 04 13:14:11 1998 +0100
     1.3 @@ -83,13 +83,11 @@
     1.4  in
     1.5  
     1.6    fun mk_meta_eq r = r RS eq_reflection;
     1.7 +  fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
     1.8  
     1.9    fun mk_meta_eq_simp r = case concl_of r of
    1.10            Const("==",_)$_$_ => r
    1.11 -      |   _$(Const("op =",_)$lhs$rhs) =>
    1.12 -             (case fst(Logic.rewrite_rule_ok (#sign(rep_thm r)) (prems_of r) lhs rhs) of
    1.13 -                None => mk_meta_eq r
    1.14 -              | Some _ => r RS P_imp_P_eq_True)
    1.15 +      |   _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
    1.16        |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    1.17        |   _ => r RS P_imp_P_eq_True;
    1.18    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.19 @@ -386,7 +384,8 @@
    1.20  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.21  			    setSSolver   safe_solver
    1.22  			    setSolver  unsafe_solver
    1.23 -			    setmksimps (mksimps mksimps_pairs);
    1.24 +			    setmksimps (mksimps mksimps_pairs)
    1.25 +			    setmkeqTrue mk_meta_eq_True;
    1.26  
    1.27  val HOL_ss = 
    1.28      HOL_basic_ss addsimps