Mercurial Mercurial > repos > isabelle / 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.
tuned proofs;
authorwenzelm
Sat, 17 May 2008 23:53:19 +0200
changeset 26937 57e7d045774a
parent 26936 faf8a5b5ba87
child 26938 64e850c3da9e
tuned proofs;
src/HOL/TLA/Memory/Memory.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/TLA/Memory/Memory.thy	Sat May 17 23:37:11 2008 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy	Sat May 17 23:53:19 2008 +0200
@@ -161,7 +161,6 @@
 lemma MemoryInvariantAll:
     "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
   apply clarify
-  apply (case_tac "l : MemLoc")
   apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
   done
isabelle