1.1 --- a/src/HOL/UNITY/Mutex.ML	Wed Sep 01 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Mutex.ML	Wed Sep 01 11:16:02 1999 +0200
     1.3 @@ -17,15 +17,11 @@
     1.4  
     1.5  
     1.6  Goal "Mutex : Always IU";
     1.7 -by (rtac AlwaysI 1);
     1.8 -by (constrains_tac 2);
     1.9 -by Auto_tac;
    1.10 +by (always_tac 1);
    1.11  qed "IU";
    1.12  
    1.13  Goal "Mutex : Always IV";
    1.14 -by (rtac AlwaysI 1);
    1.15 -by (constrains_tac 2);
    1.16 -by Auto_tac;
    1.17 +by (always_tac 1);
    1.18  qed "IV";
    1.19  
    1.20  (*The safety property: mutual exclusion*)
    1.21 @@ -38,8 +34,7 @@
    1.22  
    1.23  (*The bad invariant FAILS in V1*)
    1.24  Goal "Mutex : Always bad_IU";
    1.25 -by (rtac AlwaysI 1);
    1.26 -by (constrains_tac 2);
    1.27 +by (always_tac 1);
    1.28  by Auto_tac;
    1.29  (*Resulting state: n=1, p=false, m=4, u=false.  
    1.30    Execution of V1 (the command of process v guarded by n=1) sets p:=true,