src/ZF/ex/TF.thy
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections