--- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Oct 27 09:06:05 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Oct 27 09:24:45 2009 +0100
@@ -28,7 +28,7 @@
code_pred (mode: [], [1], [2], [1, 2])EmptyClosure .
thm EmptyClosure.equation
-
+(* TODO: inductive package is broken!
inductive False'' :: "bool"
where
"False \<Longrightarrow> False''"
@@ -41,7 +41,7 @@
code_pred (mode: [1]) EmptySet'' .
code_pred (mode: [], [1]) [inductify] EmptySet'' .
-
+*)
inductive True' :: "bool"
where
"True \<Longrightarrow> True'"