equal
deleted
inserted
replaced
|
1 (* Title: ZF/ex/Brouwer.thy |
|
2 ID: $ $ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Datatype definition of the Brouwer ordinals -- demonstrates infinite branching |
|
7 *) |
|
8 |
|
9 Brouwer = InfDatatype + |
|
10 consts |
|
11 brouwer :: "i" |
|
12 |
|
13 datatype <= "Vfrom(0, csucc(nat))" |
|
14 "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer") |
|
15 monos "[Pi_mono]" |
|
16 type_intrs "inf_datatype_intrs" |
|
17 |
|
18 end |