src/HOL/MicroJava/DFA/Listn.thy
changeset 68646 7dc9fe795dae
parent 67613 ce654b0e6d69
     1.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Mon Jul 16 23:33:38 2018 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Tue Jul 17 22:18:27 2018 +0100
     1.3 @@ -323,12 +323,10 @@
     1.4   apply (blast intro: lesssub_list_impl_same_size)
     1.5  apply (rule wf_UN)
     1.6   prefer 2
     1.7 - apply clarify
     1.8   apply (rename_tac m n)
     1.9   apply (case_tac "m=n")
    1.10    apply simp
    1.11   apply (fast intro!: equals0I dest: not_sym)
    1.12 -apply clarify
    1.13  apply (rename_tac n)
    1.14  apply (induct_tac n)
    1.15   apply (simp add: lesssub_def cong: conj_cong)
    1.16 @@ -353,7 +351,7 @@
    1.17   apply blast
    1.18  apply clarify
    1.19  apply (thin_tac "m \<in> M")
    1.20 -apply (thin_tac "maxA#xs \<in> M")
    1.21 +  apply (thin_tac "maxA#xs \<in> M")
    1.22  apply (rule bexI)
    1.23   prefer 2
    1.24   apply assumption