# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293066305 0
# Node ID 8a4c44cef353fae55a803c6bde50b70618551dbb
# Parent  d1bdc281be2b25dbcfdba33983aae82a4ffa52ff
test with strong inductions

diff -r d1bdc281be2b -r 8a4c44cef353 Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Thu Dec 23 00:46:06 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Thu Dec 23 01:05:05 2010 +0000
@@ -73,8 +73,7 @@
   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'"
-using assms
-apply(induction_schema)
+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))