src/ZF/OrderArith.thy
changeset 9883 c1c8647af477
parent 1478 2b8c2a7547ab
child 13140 6d97dbb189a9
     1.1 --- a/src/ZF/OrderArith.thy	Thu Sep 07 15:31:09 2000 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Thu Sep 07 17:36:37 2000 +0200
     1.3 @@ -3,10 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Towards ordinal arithmetic 
     1.8 +Towards ordinal arithmetic.  Also useful with wfrec.
     1.9  *)
    1.10  
    1.11 -OrderArith = Order + Sum + 
    1.12 +OrderArith = Order + Sum + Ordinal +
    1.13  consts
    1.14    radd, rmult      :: [i,i,i,i]=>i
    1.15    rvimage          :: [i,i,i]=>i
    1.16 @@ -28,4 +28,9 @@
    1.17    (*inverse image of a relation*)
    1.18    rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
    1.19  
    1.20 +constdefs
    1.21 +   measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i"
    1.22 +   "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
    1.23 +
    1.24 +
    1.25  end