src/ZF/UNITY/Increasing.thy
changeset 14055 a3f592e3f4bd
parent 14052 e9c9f69e4f63
child 14093 24382760fd89
--- a/src/ZF/UNITY/Increasing.thy	Fri May 30 11:44:29 2003 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Mon Jun 02 11:17:52 2003 +0200
@@ -12,9 +12,6 @@
 Increasing = Constrains + Monotonicity +
 constdefs
 
-  part_order :: [i, i] => o
-  "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
-
   increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')")
   "increasing[A](r, f) ==
     {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) &