Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
snapshot
authorChristian Urban <urbanc@in.tum.de>
Tue, 30 Jul 2019 10:44:12 +0100
changeset 336 44914e2724b7
parent 335 f5ab2f02d148
child 337 50bb2c83eeb1
child 340 6c71db65bdec
snapshot
thys/BitCoded.thy file | annotate | diff | comparison | revisions 
--- a/thys/BitCoded.thy	Mon Jul 29 21:39:46 2019 +0100
+++ b/thys/BitCoded.thy	Tue Jul 30 10:44:12 2019 +0100
@@ -2688,14 +2688,7 @@
     apply(simp)
   (* AALT case *)
    prefer 2
-  apply(simp only:)
-  (* *)
-  apply(simp)
-   apply(subst WWW5)
-  
-
-
-
+   apply(simp only:)
    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
     apply(clarify)
   apply(simp del: bsimp.simps)
lexing