1.1 --- a/src/HOL/UNITY/Handshake.ML	Tue May 11 10:32:10 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Handshake.ML	Tue May 11 10:32:45 1999 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  qed "invFG";
     1.5  
     1.6  Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
     1.7 -\                          ({s. NF s = k} Int {s. BB s})";
     1.8 +\                  ({s. NF s = k} Int {s. BB s})";
     1.9  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.10  by (ensures_tac "cmdG" 2);
    1.11  by (constrains_tac 1);