src/HOL/UNITY/Handshake.ML

--- a/src/HOL/UNITY/Handshake.ML	Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Tue May 04 10:26:00 1999 +0200
@@ -21,8 +21,8 @@
 Addsimps [simp_of_set invFG_def];
 
 
-Goal "(F Join G) : Invariant invFG";
-by (rtac InvariantI 1);
+Goal "(F Join G) : Always invFG";
+by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (rtac (constrains_imp_Constrains RS StableI) 1);
 by (auto_tac (claset(), simpset() addsimps [constrains_Join]));