diff -r 84e8d378eb5e -r 7621a3b42ce7 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Jun 26 22:50:02 2014 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Jun 27 00:21:11 2014 +0100
@@ -198,7 +198,7 @@
 by (metis insert_is_Un parts_Un)
 
 text{*TWO inserts to avoid looping.  This rewrite is better than nothing.
-  Not suitable for Addsimps: its behaviour can be strange.*}
+  But its behaviour can be strange.*}
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un)
@@ -310,14 +310,15 @@
 
 text{*In any message, there is an upper bound N on its greatest nonce.*}
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
-apply (induct msg)
-apply (simp_all (no_asm_simp) add: exI parts_insert2)
-txt{*Nonce case*}
-apply (metis Suc_n_not_le_n)
-txt{*MPair case: metis works out the necessary sum itself!*}
-apply (metis le_trans nat_le_linear)
-done
-
+proof (induct msg)
+  case (Nonce n)
+    show ?case
+      by simp (metis Suc_n_not_le_n)
+next
+  case (MPair X Y)
+    then show ?case --{*metis works out the necessary sum itself!*}
+      by (simp add: parts_insert2) (metis le_trans nat_le_linear)
+qed auto
 
 subsection{*Inductive relation "analz"*}
 
@@ -618,18 +619,6 @@
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 by (erule synth_trans, blast)
 
-lemma Agent_synth [simp]: "Agent A \<in> synth H"
-by blast
-
-lemma Number_synth [simp]: "Number n \<in> synth H"
-by blast
-
-lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
-by blast
-
-lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
-by blast
-
 lemma Crypt_synth_eq [simp]:
      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
 by blast
@@ -726,22 +715,22 @@
 subsubsection{*Freeness *}
 
 lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
-by (unfold HPair_def, simp)
+  unfolding HPair_def by simp
 
 lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair 
                     Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
@@ -840,9 +829,7 @@
 
 (*The key-free part of a set of messages can be removed from the scope of the analz operator.*)
 lemma analz_keyfree_into_Un: "\<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H"
-apply (erule analz.induct, auto)
-apply (blast dest:parts.Body)
-apply (blast dest: parts.Body)
+apply (erule analz.induct, auto dest: parts.Body)
 apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
 done