renamed Always_Int to Always_Int_I
authorpaulson
Mon, 20 Sep 1999 10:46:16 +0200
changeset 7543 abefbd41bd3e
parent 7542 b6599e292011
child 7544 dee529666dcd
renamed Always_Int to Always_Int_I
src/HOL/UNITY/Mutex.ML
--- 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";