Constant "If" is now local
authorpaulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587b34c8aa657a5
parent 16586 9b1b50514b5e
child 16588 8de758143786
Constant "If" is now local
src/HOL/HOL.thy
src/HOL/Import/HOL/bool.imp
src/HOL/Main.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/eqrule_HOL_data.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 28 15:26:45 2005 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 28 15:27:45 2005 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    Not           :: "bool => bool"                   ("~ _" [40] 40)
     1.5    True          :: bool
     1.6    False         :: bool
     1.7 -  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
     1.8    arbitrary     :: 'a
     1.9  
    1.10    The           :: "('a => bool) => 'a"
    1.11 @@ -49,6 +48,8 @@
    1.12  
    1.13  local
    1.14  
    1.15 +consts
    1.16 +  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
    1.17  
    1.18  subsubsection {* Additional concrete syntax *}
    1.19  
     2.1 --- a/src/HOL/Import/HOL/bool.imp	Tue Jun 28 15:26:45 2005 +0200
     2.2 +++ b/src/HOL/Import/HOL/bool.imp	Tue Jun 28 15:27:45 2005 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    "LET" > "HOL4Compat.LET"
     2.5    "IN" > "HOL4Base.bool.IN"
     2.6    "F" > "False"
     2.7 -  "COND" > "If"
     2.8 +  "COND" > "HOL.If"
     2.9    "ARB" > "HOL4Base.bool.ARB"
    2.10    "?!" > "Ex1"
    2.11    "?" > "Ex"
     3.1 --- a/src/HOL/Main.thy	Tue Jun 28 15:26:45 2005 +0200
     3.2 +++ b/src/HOL/Main.thy	Tue Jun 28 15:27:45 2005 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4    "Not"     ("not")
     3.5    "op |"    ("(_ orelse/ _)")
     3.6    "op &"    ("(_ andalso/ _)")
     3.7 -  "If"      ("(if _/ then _/ else _)")
     3.8 +  "HOL.If"      ("(if _/ then _/ else _)")
     3.9  
    3.10    "wfrec"   ("wf'_rec?")
    3.11  
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:26:45 2005 +0200
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:27:45 2005 +0200
     4.3 @@ -41,7 +41,7 @@
     4.4  local
     4.5    (* searching an if-term as below as possible *)
     4.6    fun contains_if (Abs(a,T,t)) = [] |
     4.7 -  contains_if (Const("If",T) $ b $ a1 $ a2) =
     4.8 +  contains_if (Const("HOL.If",T) $ b $ a1 $ a2) =
     4.9    let
    4.10    fun tn (Type(s,_)) = s |
    4.11    tn _ = error "cannot master type variables in if term";
    4.12 @@ -60,7 +60,7 @@
    4.13    find_replace_term t = (t,[]);
    4.14  
    4.15    fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
    4.16 -  if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
    4.17 +  if_substi (Const("HOL.If",T) $ b $ a1 $ a2) t = t |
    4.18    if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
    4.19  		        else (a$(if_substi b t)) |
    4.20    if_substi t v = t;
    4.21 @@ -654,7 +654,7 @@
    4.22    val tty = type_of_term t;
    4.23    val con_term = con_term_of con a;
    4.24   in
    4.25 -	(Const("If",Type("fun",[Type("bool",[]),
    4.26 +	(Const("HOL.If",Type("fun",[Type("bool",[]),
    4.27          Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
    4.28  	(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
    4.29          t $ con_term) $
    4.30 @@ -757,7 +757,7 @@
    4.31   fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
    4.32   casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
    4.33   casc_if2 sg tl x con (a::r) ty trm cl =
    4.34 -        Const("If",Type("fun",[Type("bool",[]),
    4.35 +        Const("HOL.If",Type("fun",[Type("bool",[]),
    4.36          Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
    4.37          ])) $
    4.38       (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $
     5.1 --- a/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:26:45 2005 +0200
     5.2 +++ b/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:27:45 2005 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  val tranformation_pairs =
     5.5    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
     5.6     ("All", [spec]), ("True", []), ("False", []),
     5.7 -   ("If", [if_bool_eq_conj RS iffD1])];
     5.8 +   ("HOL.If", [if_bool_eq_conj RS iffD1])];
     5.9  
    5.10  (*
    5.11  val mk_atomize:      (string * thm list) list -> thm -> thm list
     6.1 --- a/src/HOL/simpdata.ML	Tue Jun 28 15:26:45 2005 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Tue Jun 28 15:27:45 2005 +0200
     6.3 @@ -240,7 +240,7 @@
     6.4  val mksimps_pairs =
     6.5    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
     6.6     ("All", [spec]), ("True", []), ("False", []),
     6.7 -   ("If", [if_bool_eq_conj RS iffD1])];
     6.8 +   ("HOL.If", [if_bool_eq_conj RS iffD1])];
     6.9  
    6.10  (*
    6.11  val mk_atomize:      (string * thm list) list -> thm -> thm list