src/HOL/Product_Type.thy
changeset 25534 d0b74fdd6067
parent 25511 54db9b5080b8
child 25885 6fbc3f54f819
     1.1 --- a/src/HOL/Product_Type.thy	Wed Dec 05 14:15:39 2007 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Dec 05 14:15:45 2007 +0100
     1.3 @@ -24,6 +24,17 @@
     1.4  declare case_split [cases type: bool]
     1.5    -- "prefer plain propositional version"
     1.6  
     1.7 +lemma [code func]:
     1.8 +  shows "False = P \<longleftrightarrow> \<not> P"
     1.9 +    and "True = P \<longleftrightarrow> P" 
    1.10 +    and "P = False \<longleftrightarrow> \<not> P" 
    1.11 +    and "P = True \<longleftrightarrow> P" by simp_all
    1.12 +
    1.13 +code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.14 +  (Haskell infixl 4 "==")
    1.15 +
    1.16 +code_instance bool :: eq
    1.17 +  (Haskell -)
    1.18  
    1.19  subsection {* Unit *}
    1.20