src/HOL/Datatype.thy
changeset 19817 bb16bf9ae3fd
parent 19787 b949911ecff5
child 19890 1aad48bcc674
     1.1 --- a/src/HOL/Datatype.thy	Wed Jun 07 16:54:30 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jun 07 16:55:14 2006 +0200
     1.3 @@ -219,20 +219,20 @@
     1.4    done
     1.5  
     1.6  
     1.7 +subsubsection {* Codegenerator setup *}
     1.8 +
     1.9  consts
    1.10    is_none :: "'a option \<Rightarrow> bool"
    1.11  primrec
    1.12    "is_none None = True"
    1.13    "is_none (Some x) = False"
    1.14  
    1.15 -(* lemma is_none_none [code unfolt]:
    1.16 +lemma is_none_none [code unfolt]:
    1.17    "(x = None) = (is_none x)" 
    1.18 -by (cases "x") simp_all *)
    1.19 +by (cases "x") simp_all
    1.20  
    1.21  lemmas [code] = imp_conv_disj
    1.22  
    1.23 -subsubsection {* Codegenerator setup *}
    1.24 -
    1.25  lemma [code fun]:
    1.26    "(\<not> True) = False" by (rule HOL.simp_thms)
    1.27  
    1.28 @@ -260,8 +260,6 @@
    1.29  lemma [code unfolt]:
    1.30    "1 == Suc 0" by simp
    1.31  
    1.32 -code_generate True False Not "op &" "op |" If
    1.33 -
    1.34  code_syntax_tyco bool
    1.35    ml (target_atom "bool")
    1.36    haskell (target_atom "Bool")
    1.37 @@ -286,8 +284,6 @@
    1.38      ml (target_atom "(if __/ then __/ else __)")
    1.39      haskell (target_atom "(if __/ then __/ else __)")
    1.40  
    1.41 -code_generate Pair
    1.42 -
    1.43  code_syntax_tyco
    1.44    *
    1.45      ml (infix 2 "*")
    1.46 @@ -298,8 +294,6 @@
    1.47      ml (target_atom "(__,/ __)")
    1.48      haskell (target_atom "(__,/ __)")
    1.49  
    1.50 -code_generate Unity
    1.51 -
    1.52  code_syntax_tyco
    1.53    unit
    1.54      ml (target_atom "unit")
    1.55 @@ -310,8 +304,6 @@
    1.56      ml (target_atom "()")
    1.57      haskell (target_atom "()")
    1.58  
    1.59 -code_generate None Some
    1.60 -
    1.61  code_syntax_tyco
    1.62    option
    1.63      ml ("_ option")
    1.64 @@ -325,7 +317,4 @@
    1.65      ml (target_atom "SOME")
    1.66      haskell (target_atom "Just")
    1.67  
    1.68 -
    1.69 -
    1.70 -
    1.71  end