Renamed constant "not" to "Not"
authorpaulson
Tue Mar 04 10:48:36 1997 +0100 (1997-03-04)
changeset 2718460fd0f8d478
parent 2717 b29c45ef3d86
child 2719 27167b432e7a
Renamed constant "not" to "Not"
src/HOL/NatDef.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/NatDef.ML	Tue Mar 04 10:42:28 1997 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Tue Mar 04 10:48:36 1997 +0100
     1.3 @@ -667,7 +667,7 @@
     1.4    | negate None = None;
     1.5  
     1.6  fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
     1.7 -  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
     1.8 +  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
     1.9        negate(decomp2(rel,T,lhs,rhs))
    1.10    | decomp _ = None
    1.11  
     2.1 --- a/src/HOL/simpdata.ML	Tue Mar 04 10:42:28 1997 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Tue Mar 04 10:48:36 1997 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4  
     2.5    fun addIff th = 
     2.6        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
     2.7 -                (Const("not",_) $ A) =>
     2.8 +                (Const("Not",_) $ A) =>
     2.9                      AddSEs [zero_var_indexes (th RS notE)]
    2.10                | (con $ _ $ _) =>
    2.11                      if con=iff_const
    2.12 @@ -36,7 +36,7 @@
    2.13  
    2.14    fun delIff th = 
    2.15        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    2.16 -                (Const("not",_) $ A) =>
    2.17 +                (Const("Not",_) $ A) =>
    2.18                      Delrules [zero_var_indexes (th RS notE)]
    2.19                | (con $ _ $ _) =>
    2.20                      if con=iff_const
    2.21 @@ -83,7 +83,7 @@
    2.22    fun mk_meta_eq r = case concl_of r of
    2.23            Const("==",_)$_$_ => r
    2.24        |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    2.25 -      |   _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
    2.26 +      |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    2.27        |   _ => r RS P_imp_P_eq_True;
    2.28    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    2.29