diff -r 66c941ea1f01 -r a7d7985050a9 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Tue May 04 10:26:00 1999 +0200
@@ -46,8 +46,9 @@
   Stable     :: "'a set => 'a program set"
     "Stable A == A Co A"
 
-  Invariant :: "'a set => 'a program set"
-    "Invariant A == {F. Init F <= A} Int Stable A"
+  (*Always is the weak form of "invariant"*)
+  Always :: "'a set => 'a program set"
+    "Always A == {F. Init F <= A} Int Stable A"
 
   (*Polymorphic in both states and the meaning of <= *)
   Increasing :: "['a => 'b::{ord}] => 'a program set"