src/CCL/Wfd.thy
changeset 36319 8feb2c4bef1a
parent 33317 b4534348b8fd
child 38500 d5477ee35820
--- a/src/CCL/Wfd.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CCL/Wfd.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -573,29 +573,29 @@
 
 subsection {* Factorial *}
 
-lemma
+schematic_lemma
   "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    in f(succ(succ(zero))) ---> ?a"
   by eval
 
-lemma
+schematic_lemma
   "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    in f(succ(succ(succ(zero)))) ---> ?a"
   by eval
 
 subsection {* Less Than Or Equal *}
 
-lemma
+schematic_lemma
   "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    in f(<succ(zero), succ(zero)>) ---> ?a"
   by eval
 
-lemma
+schematic_lemma
   "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
   by eval
 
-lemma
+schematic_lemma
   "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
   by eval
@@ -603,12 +603,12 @@
 
 subsection {* Reverse *}
 
-lemma
+schematic_lemma
   "letrec id l be lcase(l,[],%x xs. x$id(xs))  
    in id(zero$succ(zero)$[]) ---> ?a"
   by eval
 
-lemma
+schematic_lemma
   "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))  
    in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
   by eval