# HG changeset patch
# User paulson
# Date 857468916 -3600
# Node ID 460fd0f8d478a8f886c1eaa07c5135d6e8aced4e
# Parent  b29c45ef3d86c613585b593297bd0e34c2453ee2
Renamed constant "not" to "Not"

diff -r b29c45ef3d86 -r 460fd0f8d478 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Mar 04 10:42:28 1997 +0100
+++ b/src/HOL/NatDef.ML	Tue Mar 04 10:48:36 1997 +0100
@@ -667,7 +667,7 @@
   | negate None = None;
 
 fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
-  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
+  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
       negate(decomp2(rel,T,lhs,rhs))
   | decomp _ = None
 
diff -r b29c45ef3d86 -r 460fd0f8d478 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Mar 04 10:42:28 1997 +0100
+++ b/src/HOL/simpdata.ML	Tue Mar 04 10:48:36 1997 +0100
@@ -22,7 +22,7 @@
 
   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
@@ -36,7 +36,7 @@
 
   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
@@ -83,7 +83,7 @@
   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(.) *)