--- a/Nominal/Ex/Foo1.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -44,6 +44,7 @@
 thm foo.induct
 thm foo.inducts
 thm foo.exhaust
+thm foo.strong_induct
 thm foo.strong_exhaust
 thm foo.fv_defs
 thm foo.bn_defs
@@ -57,32 +58,6 @@
 thm foo.fresh
 thm foo.bn_finite
 
-lemma 
-  fixes t::trm
-  and   as::assg
-  and   as'::assg'
-  and   c::"'a::fs"
-  assumes a1: "\<And>x c. P1 c (Var x)"
-  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
-  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
-  and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"
-  and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"
-  and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"
-  and     a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" 
-  and     a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
-  and     a9: "\<And>c. P3 c (BNil)"
-  and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
-  shows "P1 c t" "P2 c as" "P3 c as'"
-apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
-apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))
-apply(simp_all)[7]
-apply(rule_tac ya="as"in foo.strong_exhaust(2))
-apply(simp_all)[1]
-apply(rule_tac yb="as'" in foo.strong_exhaust(3))
-apply(simp_all)[2]
-apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))")
-apply(simp_all add: foo.size)
-done
 
 end