--- 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"