src/HOL/Product_Type.thy
changeset 28562 4e74209f113e
parent 28537 1e84256d1a8a
child 28719 01e04e41cc7b
     1.1 --- a/src/HOL/Product_Type.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -23,10 +23,10 @@
     1.4    -- "prefer plain propositional version"
     1.5  
     1.6  lemma
     1.7 -  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
     1.8 -    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
     1.9 -    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
    1.10 -    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
    1.11 +  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
    1.12 +    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
    1.13 +    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
    1.14 +    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
    1.15      and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
    1.16    by (simp_all add: eq)
    1.17  
    1.18 @@ -89,7 +89,7 @@
    1.19  
    1.20  instance unit :: eq ..
    1.21  
    1.22 -lemma [code func]:
    1.23 +lemma [code]:
    1.24    "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
    1.25  
    1.26  code_type unit
    1.27 @@ -359,10 +359,10 @@
    1.28  
    1.29  subsubsection {* @{text split} and @{text curry} *}
    1.30  
    1.31 -lemma split_conv [simp, code func]: "split f (a, b) = f a b"
    1.32 +lemma split_conv [simp, code]: "split f (a, b) = f a b"
    1.33    by (simp add: split_def)
    1.34  
    1.35 -lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
    1.36 +lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
    1.37    by (simp add: curry_def)
    1.38  
    1.39  lemmas split = split_conv  -- {* for backwards compatibility *}
    1.40 @@ -728,9 +728,9 @@
    1.41  *}
    1.42  
    1.43  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    1.44 -  [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    1.45 +  [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    1.46  
    1.47 -lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
    1.48 +lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
    1.49    by (simp add: prod_fun_def)
    1.50  
    1.51  lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
    1.52 @@ -758,12 +758,12 @@
    1.53  definition
    1.54    apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
    1.55  where
    1.56 -  [code func del]: "apfst f = prod_fun f id"
    1.57 +  [code del]: "apfst f = prod_fun f id"
    1.58  
    1.59  definition
    1.60    apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
    1.61  where
    1.62 -  [code func del]: "apsnd f = prod_fun id f"
    1.63 +  [code del]: "apsnd f = prod_fun id f"
    1.64  
    1.65  lemma apfst_conv [simp, code]:
    1.66    "apfst f (x, y) = (f x, y)" 
    1.67 @@ -917,7 +917,7 @@
    1.68  
    1.69  instance * :: (eq, eq) eq ..
    1.70  
    1.71 -lemma [code func]:
    1.72 +lemma [code]:
    1.73    "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
    1.74  
    1.75  lemma split_case_cert: