Mercurial Mercurial > hg > lexing / 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.
thys/Sulzmann.thy
changeset 313 3b8e3a156200
parent 307 ee1caac29bb2
child 362 e51c9a67a68d 
--- a/thys/Sulzmann.thy	Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/Sulzmann.thy	Sat Feb 23 21:52:06 2019 +0000
@@ -247,6 +247,12 @@
   shows "bmkeps r = retrieve r (mkeps (erase r))"
   using assms
   apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp) 
+   apply(simp only: bmkeps.simps bnullable_correctness)
+  apply(auto simp only: split: if_split)
   apply(auto simp add: bnullable_correctness)
   done
lexing