--- a/src/HOL/MicroJava/DFA/Listn.thy Mon Jul 16 23:33:38 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Tue Jul 17 22:18:27 2018 +0100
@@ -323,12 +323,10 @@
apply (blast intro: lesssub_list_impl_same_size)
apply (rule wf_UN)
prefer 2
- apply clarify
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
apply (fast intro!: equals0I dest: not_sym)
-apply clarify
apply (rename_tac n)
apply (induct_tac n)
apply (simp add: lesssub_def cong: conj_cong)
@@ -353,7 +351,7 @@
apply blast
apply clarify
apply (thin_tac "m \<in> M")
-apply (thin_tac "maxA#xs \<in> M")
+ apply (thin_tac "maxA#xs \<in> M")
apply (rule bexI)
prefer 2
apply assumption