--- a/src/HOL/Code_Generator.thy Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Code_Generator.thy Fri Mar 09 08:45:53 2007 +0100
@@ -87,7 +87,9 @@
(Haskell infixl 4 "==")
-text {* boolean expressions *}
+text {* type bool *}
+
+code_datatype True False
lemma [code func]:
shows "(False \<and> x) = False"
@@ -152,18 +154,22 @@
bool true false not
-text {* itself as a code generator datatype *}
+text {* type prop *}
+
+code_datatype Trueprop "prop"
+
+
+text {* type itself *}
-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
-*}
+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 *}