--- a/src/ZF/OrderArith.thy Thu Sep 07 15:31:09 2000 +0200
+++ b/src/ZF/OrderArith.thy Thu Sep 07 17:36:37 2000 +0200
@@ -3,10 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Towards ordinal arithmetic
+Towards ordinal arithmetic. Also useful with wfrec.
*)
-OrderArith = Order + Sum +
+OrderArith = Order + Sum + Ordinal +
consts
radd, rmult :: [i,i,i,i]=>i
rvimage :: [i,i,i]=>i
@@ -28,4 +28,9 @@
(*inverse image of a relation*)
rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
+constdefs
+ measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i"
+ "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
+
+
end