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.
modernized dead code;
authorwenzelm
Thu, 12 May 2011 22:35:15 +0200
changeset 42772 2acb503fd857
parent 42771 b6037ae5027d
child 42773 29042b3e7575
modernized dead code;
src/HOL/TLA/Memory/MemoryImplementation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu May 12 22:33:38 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu May 12 22:35:15 2011 +0200
@@ -294,11 +294,9 @@
 *)
 
 (* --- not used ---
-Goal "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
-                         ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
-by (auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def,
-                                S3_def, S4_def, S5_def, S6_def]));
-qed "S1_excl";
+lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
+    ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
+  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 *)
 
 lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
isabelle