diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Client.thy	Thu Oct 15 11:35:07 1998 +0200
@@ -8,24 +8,6 @@
 
 Client = Comp + Prefix + 
 
-constdefs  (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
-  always :: "'a set => 'a program set"
-    "always A == {F. reachable F <= A}"
-
-  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
-    reserved!*)
-  invariant :: "'a set => 'a program set"
-    "invariant A == {F. Init F <= A & stable (Acts F) A}"
-
-  (*Polymorphic in both states and the meaning of <= *)
-  increasing :: "['a => 'b::{ord}] => 'a program set"
-    "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}"
-
-  (*The set of systems that regard "f" as local to F*)
-  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
-    "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}"
-
-
 consts
   Max :: nat       (*Maximum number of tokens*)