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})) &