# HG changeset patch
# User wenzelm
# Date 1433949755 -7200
# Node ID e1ff959f4f1b3fe03874e8319d0b75706cd5ee3b
# Parent  9d37b2330ee383292c3319c66f88061ed9865f90
tuned proofs;

diff -r 9d37b2330ee3 -r e1ff959f4f1b src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 17:22:35 2015 +0200
@@ -220,18 +220,13 @@
 proof -
   let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
   let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
   show ?thesis
   proof hoare
     show "?inv 0 1" by simp
-  next
-    fix s i
-    assume "?inv s i \<and> i \<noteq> n"
-    then show "?inv (s + i) (i + 1)" by simp
-  next
-    fix s i
-    assume "?inv s i \<and> \<not> i \<noteq> n"
-    then show "s = ?sum n" by simp
+    show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
+      using prems by simp
+    show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
+      using prems by simp
   qed
 qed
 
diff -r 9d37b2330ee3 -r e1ff959f4f1b src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 17:22:35 2015 +0200
@@ -208,9 +208,8 @@
   let ?e = evnodd
   note hyp = \<open>card (?e t 0) = card (?e t 1)\<close>
     and at = \<open>a \<subseteq> - t\<close>
-  have card_suc: "b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))" for b :: nat
+  have card_suc: "card (?e (a \<union> t) b) = Suc (card (?e t b))" if "b < 2" for b :: nat
   proof -
-    assume "b < 2"
     have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
     also obtain i j where e: "?e a b = {(i, j)}"
     proof -
diff -r 9d37b2330ee3 -r e1ff959f4f1b src/HOL/Isar_Examples/Nested_Datatype.thy
--- 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