--- a/src/Tools/Nbe/Nbe.thy Fri Jul 27 10:09:44 2007 +0200
+++ b/src/Tools/Nbe/Nbe.thy Fri Jul 27 10:18:56 2007 +0200
@@ -11,6 +11,11 @@
"~~/src/Tools/Nbe/nbe_package.ML"
begin
+lemma [code inline]: "If b f g = bool_case f g b" by auto
+lemma [code func]: "null xs \<longleftrightarrow> (case xs of [] \<Rightarrow> True | _ \<Rightarrow> False)"
+by (cases xs) auto
+
+
ML {* reset Toplevel.debug *}
setup Nbe_Package.setup
@@ -39,11 +44,6 @@
hide (open) const if_delayed
-lemma [code func]: "null xs \<longleftrightarrow> (case xs of [] \<Rightarrow> True | _ \<Rightarrow> False)"
-apply (cases xs) apply auto done
-
-normal_form "null [x]"
-
lemma "True"
by normalization
lemma "x = x" by normalization
@@ -163,6 +163,6 @@
normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-
lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
+lemma "null [x] = False" by normalization
\ No newline at end of file