--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 17:22:35 2015 +0200
@@ -37,17 +37,12 @@
subst_term_list f1 (subst_term_list f2 ts)"
show ?thesis
proof (induct t rule: subst_term.induct)
- fix a show "?P (Var a)" by simp
- next
- fix b ts assume "?Q ts"
- then show "?P (App b ts)"
- by (simp only: subst_simps)
- next
+ show "?P (Var a)" for a by simp
+ show "?P (App b ts)" if "?Q ts" for b ts
+ using prems by (simp only: subst_simps)
show "?Q []" by simp
- next
- fix t ts
- assume "?P t" "?Q ts" then show "?Q (t # ts)"
- by (simp only: subst_simps)
+ show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
+ using prems by (simp only: subst_simps)
qed
qed