# HG changeset patch
# User paulson
# Date 926411565 -7200
# Node ID 3f807540e93940d0c44635f8f02d749c1b009674
# Parent  ccae8c659762c31b26ee5f3b701a9429d82583ff
tidied

diff -r ccae8c659762 -r 3f807540e939 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Tue May 11 10:32:10 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Tue May 11 10:32:45 1999 +0200
@@ -32,7 +32,7 @@
 qed "invFG";
 
 Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
-\                          ({s. NF s = k} Int {s. BB s})";
+\                  ({s. NF s = k} Int {s. BB s})";
 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (ensures_tac "cmdG" 2);
 by (constrains_tac 1);