src/ZF/ex/Brouwer.thy
1994-08-15 lcp 1994-08-15 ZF/ex/Brouwer.thy,.ML: new example of wellordering types
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections