src/CTT/ex/Typechecking.thy

--- a/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -11,18 +11,18 @@
 
 subsection {* Single-step proofs: verifying that a type is well-formed *}
 
-lemma "?A type"
+schematic_lemma "?A type"
 apply (rule form_rls)
 done
 
-lemma "?A type"
+schematic_lemma "?A type"
 apply (rule form_rls)
 back
 apply (rule form_rls)
 apply (rule form_rls)
 done
 
-lemma "PROD z:?A . N + ?B(z) type"
+schematic_lemma "PROD z:?A . N + ?B(z) type"
 apply (rule form_rls)
 apply (rule form_rls)
 apply (rule form_rls)
@@ -37,30 +37,30 @@
 apply (tactic form_tac)
 done
 
-lemma "<0, succ(0)> : ?A"
+schematic_lemma "<0, succ(0)> : ?A"
 apply (tactic "intr_tac []")
 done
 
-lemma "PROD w:N . Eq(?A,w,w) type"
+schematic_lemma "PROD w:N . Eq(?A,w,w) type"
 apply (tactic "typechk_tac []")
 done
 
-lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
 apply (tactic "typechk_tac []")
 done
 
 text "typechecking an application of fst"
-lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
+schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
 apply (tactic "typechk_tac []")
 done
 
 text "typechecking the predecessor function"
-lemma "lam n. rec(n, 0, %x y. x) : ?A"
+schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
 apply (tactic "typechk_tac []")
 done
 
 text "typechecking the addition function"
-lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
+schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
 apply (tactic "typechk_tac []")
 done
 
@@ -68,18 +68,18 @@
   For concreteness, every type variable left over is forced to be N*)
 ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
 
-lemma "lam w. <w,w> : ?A"
+schematic_lemma "lam w. <w,w> : ?A"
 apply (tactic "typechk_tac []")
 apply (tactic N_tac)
 done
 
-lemma "lam x. lam y. x : ?A"
+schematic_lemma "lam x. lam y. x : ?A"
 apply (tactic "typechk_tac []")
 apply (tactic N_tac)
 done
 
 text "typechecking fst (as a function object)"
-lemma "lam i. split(i, %j k. j) : ?A"
+schematic_lemma "lam i. split(i, %j k. j) : ?A"
 apply (tactic "typechk_tac []")
 apply (tactic N_tac)
 done