src/HOL/UNITY/Mutex.ML
changeset 7543 abefbd41bd3e
parent 7403 c318acb88251
child 8355 04d0f732e24e
--- a/src/HOL/UNITY/Mutex.ML	Mon Sep 20 10:45:30 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Mon Sep 20 10:46:16 1999 +0200
@@ -27,7 +27,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) 1);
+by (rtac ([IU, IV] MRS Always_Int_I) 1);
 by Auto_tac;
 qed "mutual_exclusion";