src/HOL/Code_Generator.thy

 
 code_const "op ="
   (Haskell infixl 4 "==")
 
 
-text {* boolean expressions *}
+text {* type bool *}
+
+code_datatype True False
 
 lemma [code func]:
   shows "(False \<and> x) = False"
     and "(True \<and> x) = x"
     and "(x \<and> False) = False"

 
 code_reserved OCaml
   bool true false not
 
 
-text {* itself as a code generator datatype *}
-
-setup {*
-  let
-    val v = ("'a", []);
-    val t = Logic.mk_type (TFree v);
-    val Const (c, ty) = t;
-    val (_, Type (dtco, _)) = strip_type ty;
-  in
-    CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
-  end
-*} 
+text {* type prop *}
+
+code_datatype Trueprop "prop"
+
+
+text {* type itself *}
+
+code_datatype "TYPE('a)"
+
+
+text {* prevent unfolding of quantifier definitions *}
+
+lemma [code func]:
+  "Ex = Ex"
+  "All = All"
+  by rule+
 
 
 text {* code generation for arbitrary as exception *}
 
 setup {*