# HG changeset patch
# User paulson
# Date 952528630 -3600
# Node ID 04d0f732e24ea9a51de188213f373c6e8619c33c
# Parent  c02e3c131eca97139bcbe139b51dfddf6f8ea9bb
tidied

diff -r c02e3c131eca -r 04d0f732e24e src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Wed Mar 08 16:15:41 2000 +0100
+++ b/src/HOL/UNITY/Mutex.ML	Wed Mar 08 16:17:10 2000 +0100
@@ -26,8 +26,7 @@
 
 (*The safety property: mutual exclusion*)
 Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
-by (rtac Always_weaken 1);
-by (rtac ([IU, IV] MRS Always_Int_I) 1);
+by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
 by Auto_tac;
 qed "mutual_exclusion";