--- a/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 20:19:37 2012 +0200
@@ -225,7 +225,7 @@
assumes a: "x\<sharp>\<theta>"
shows "\<theta><Var x> = Var x"
using a
-by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
+by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm)
lemma psubst_subst_propagate:
assumes "x\<sharp>\<theta>"
@@ -529,7 +529,7 @@
lemma alg_path_equiv_implies_valid:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
-by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
+by (induct rule : alg_equiv_alg_path_equiv.inducts) auto
lemma algorithmic_symmetry:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T"
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 20:19:37 2012 +0200
@@ -140,12 +140,12 @@
lemma finite_vrs:
shows "finite (tyvrs_of x)"
and "finite (vrs_of x)"
-by (nominal_induct rule:binding.strong_induct, auto)
+by (nominal_induct rule:binding.strong_induct) auto
lemma finite_doms:
shows "finite (ty_dom \<Gamma>)"
and "finite (trm_dom \<Gamma>)"
-by (induct \<Gamma>, auto simp add: finite_vrs)
+by (induct \<Gamma>) (auto simp add: finite_vrs)
lemma ty_dom_supp:
shows "(supp (ty_dom \<Gamma>)) = (ty_dom \<Gamma>)"
@@ -155,13 +155,13 @@
lemma ty_dom_inclusion:
assumes a: "(TVarB X T)\<in>set \<Gamma>"
shows "X\<in>(ty_dom \<Gamma>)"
-using a by (induct \<Gamma>, auto)
+using a by (induct \<Gamma>) (auto)
lemma ty_binding_existence:
assumes "X \<in> (tyvrs_of a)"
shows "\<exists>T.(TVarB X T=a)"
using assms
-by (nominal_induct a rule: binding.strong_induct, auto)
+by (nominal_induct a rule: binding.strong_induct) (auto)
lemma ty_dom_existence:
assumes a: "X\<in>(ty_dom \<Gamma>)"
@@ -176,7 +176,7 @@
lemma doms_append:
shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
and "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
- by (induct \<Gamma>, auto)
+ by (induct \<Gamma>) (auto)
lemma ty_vrs_prm_simp:
fixes pi::"vrs prm"
@@ -1069,7 +1069,7 @@
lemma typing_ok:
assumes "\<Gamma> \<turnstile> t : T"
shows "\<turnstile> \<Gamma> ok"
-using assms by (induct, auto)
+using assms by (induct) (auto)
nominal_inductive typing
by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
@@ -1208,7 +1208,7 @@
lemma ty_dom_cons:
shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
-by (induct \<Gamma>, auto)
+by (induct \<Gamma>) (auto)
lemma closed_in_cons:
assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
@@ -1251,7 +1251,7 @@
lemma ty_dom_vrs:
shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
-by (induct G, auto)
+by (induct G) (auto)
lemma valid_cons':
assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
--- a/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 20:19:37 2012 +0200
@@ -321,7 +321,7 @@
proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct)
case (b_Lam x e t\<^isub>2)
have "Lam [x].e \<Down> t\<^isub>2" by fact
- thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject)
+ thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject)
next
case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2)
have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact