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