src/HOL/Product_Type.thy
changeset 38857 97775f3e8722
parent 38715 6513ea67d95d
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Product_Type.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -21,17 +21,17 @@
     1.4    -- "prefer plain propositional version"
     1.5  
     1.6  lemma
     1.7 -  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
     1.8 -    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
     1.9 -    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
    1.10 -    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
    1.11 -    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
    1.12 -  by (simp_all add: eq)
    1.13 +  shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
    1.14 +    and [code]: "HOL.equal True P \<longleftrightarrow> P" 
    1.15 +    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 
    1.16 +    and [code]: "HOL.equal P True \<longleftrightarrow> P"
    1.17 +    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    1.18 +  by (simp_all add: equal)
    1.19  
    1.20 -code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.21 +code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.22    (Haskell infixl 4 "==")
    1.23  
    1.24 -code_instance bool :: eq
    1.25 +code_instance bool :: equal
    1.26    (Haskell -)
    1.27  
    1.28  
    1.29 @@ -92,7 +92,7 @@
    1.30  end
    1.31  
    1.32  lemma [code]:
    1.33 -  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
    1.34 +  "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
    1.35  
    1.36  code_type unit
    1.37    (SML "unit")
    1.38 @@ -106,10 +106,10 @@
    1.39    (Haskell "()")
    1.40    (Scala "()")
    1.41  
    1.42 -code_instance unit :: eq
    1.43 +code_instance unit :: equal
    1.44    (Haskell -)
    1.45  
    1.46 -code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.47 +code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.48    (Haskell infixl 4 "==")
    1.49  
    1.50  code_reserved SML
    1.51 @@ -277,10 +277,10 @@
    1.52    (Haskell "!((_),/ (_))")
    1.53    (Scala "!((_),/ (_))")
    1.54  
    1.55 -code_instance prod :: eq
    1.56 +code_instance prod :: equal
    1.57    (Haskell -)
    1.58  
    1.59 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.60 +code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.61    (Haskell infixl 4 "==")
    1.62  
    1.63  types_code