src/HOL/simpdata.ML

 local
   val iff_const = HOLogic.eq_const HOLogic.boolT;
 
   fun addIff th = 
       (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
-                (Const("not",_) $ A) =>
+                (Const("Not",_) $ A) =>
                     AddSEs [zero_var_indexes (th RS notE)]
               | (con $ _ $ _) =>
                     if con=iff_const
                     then (AddSIs [zero_var_indexes (th RS iffD2)];  
                           AddSDs [zero_var_indexes (th RS iffD1)])

       handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
                          string_of_thm th)
 
   fun delIff th = 
       (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
-                (Const("not",_) $ A) =>
+                (Const("Not",_) $ A) =>
                     Delrules [zero_var_indexes (th RS notE)]
               | (con $ _ $ _) =>
                     if con=iff_const
                     then Delrules [zero_var_indexes (th RS iffD2),
                                    zero_var_indexes (th RS iffD1)]

 in
 
   fun mk_meta_eq r = case concl_of r of
           Const("==",_)$_$_ => r
       |   _$(Const("op =",_)$_$_) => r RS eq_reflection
-      |   _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
+      |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
       |   _ => r RS P_imp_P_eq_True;
   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
 
 val simp_thms = map prover
  [ "(x=x) = True",