author urbanc Wed, 11 Jan 2006 18:39:19 +0100 changeset 18660 9968dc816cda parent 18659 2ff0ae57431d child 18661 dde117622dac
cahges to use the new induction-principle (now proved in full glory)
```--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 18:38:32 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 18:39:19 2006 +0100
@@ -455,7 +455,7 @@
and b: "T closed_in \<Gamma>"
shows "\<Gamma> \<turnstile> T <: T"
using a b
-proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
+proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
case (Forall X T\<^isub>1 T\<^isub>2)
have ih_T\<^isub>1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact
have ih_T\<^isub>2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
@@ -478,7 +478,7 @@
and     b: "T closed_in \<Gamma>"
shows "\<Gamma> \<turnstile> T <: T"
using a b
-apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
+apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
--{* Too bad that this instantiation cannot be found automatically by
\isakeyword{auto}; \isakeyword{blast} would find it if we had not used ```