diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/Arith.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -256,7 +256,8 @@
 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   An example of induction over a quantified formula (a product).
   Uses rewriting with a quantified, implicative inductive hypothesis.*)
-lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+schematic_lemma add_diff_inverse_lemma:
+  "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
 apply (tactic {* NE_tac @{context} "b" 1 *})
 (*strip one "universal quantifier" but not the "implication"*)
 apply (rule_tac [3] intr_rls)
@@ -324,7 +325,7 @@
 done
 
 (*If a+b=0 then a=0.   Surprisingly tedious*)
-lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
+schematic_lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
 apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (rule_tac [3] replace_type)
 apply (tactic "arith_rew_tac []")
@@ -344,7 +345,7 @@
 done
 
 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-lemma absdiff_eq0_lem:
+schematic_lemma absdiff_eq0_lem:
     "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
      ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
 apply (unfold absdiff_def)