src/HOL/simpdata.ML
changeset 2718 460fd0f8d478
parent 2636 4b30dbe4a020
child 2748 3ae9ccdd701e
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 04 10:42:28 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Mar 04 10:48:36 1997 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5    fun addIff th = 
     1.6        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
     1.7 -                (Const("not",_) $ A) =>
     1.8 +                (Const("Not",_) $ A) =>
     1.9                      AddSEs [zero_var_indexes (th RS notE)]
    1.10                | (con $ _ $ _) =>
    1.11                      if con=iff_const
    1.12 @@ -36,7 +36,7 @@
    1.13  
    1.14    fun delIff th = 
    1.15        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    1.16 -                (Const("not",_) $ A) =>
    1.17 +                (Const("Not",_) $ A) =>
    1.18                      Delrules [zero_var_indexes (th RS notE)]
    1.19                | (con $ _ $ _) =>
    1.20                      if con=iff_const
    1.21 @@ -83,7 +83,7 @@
    1.22    fun mk_meta_eq r = case concl_of r of
    1.23            Const("==",_)$_$_ => r
    1.24        |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    1.25 -      |   _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
    1.26 +      |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    1.27        |   _ => r RS P_imp_P_eq_True;
    1.28    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.29