# HG changeset patch
# User haftmann
# Date 1185524336 -7200
# Node ID 393dd64d0d04d65d53e3a8aeb4bffcea92d0d486
# Parent  694fbb0871eb9e73dc2aaa4b0f7f012f66c9ba29
*** empty log message ***

diff -r 694fbb0871eb -r 393dd64d0d04 src/Tools/Nbe/Nbe.thy
--- 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