src/ZF/indrule.thy
1996-05-08 paulson 1996-05-08 Predicates are now uncurried in both induction rules, regardless of how tuples are nested. Only returns mutual_induct if there is true mutual recursion.
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files