--- a/src/HOL/UNITY/UNITY.thy Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/UNITY.thy Fri Nov 06 13:20:29 1998 +0100
@@ -24,15 +24,9 @@
unless :: "['a set, 'a set] => 'a program set"
"unless A B == constrains (A-B) (A Un B)"
- (*The traditional word for inductive properties. Anyway, INDUCTIVE is
- reserved!*)
invariant :: "'a set => 'a program set"
"invariant A == {F. Init F <= A} Int stable A"
- (*Safety properties*)
- always :: "'a set => 'a program set"
- "always A == {F. reachable F <= A}"
-
(*Polymorphic in both states and the meaning of <= *)
increasing :: "['a => 'b::{ord}] => 'a program set"
"increasing f == INT z. stable {s. z <= f s}"