author | lcp |
Tue, 29 Nov 1994 00:31:31 +0100 | |
changeset 753 | ec86863e87c8 |
parent 467 | 92868dab2939 |
child 850 | a744f9749885 |
permissions | -rw-r--r-- |
(* Title: ZF/OrderType.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Order types. The order type of a well-ordering is the least ordinal isomorphic to it. *) OrderType = OrderArith + Ordinal + consts ordermap :: "[i,i]=>i" ordertype :: "[i,i]=>i" defs ordermap_def "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" ordertype_def "ordertype(A,r) == ordermap(A,r)``A" end