Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/DFA/Listn.thy
changeset 68646 7dc9fe795dae
parent 67613 ce654b0e6d69 
--- 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
isabelle