src/HOL/ex/Recdef.ML
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Tue, 05 Aug 1997 16:22:17 +0200 nipkow Added example mapf which requires a special congruence rule.
Fri, 06 Jun 1997 10:18:46 +0200 paulson New example theory: Recdef
less more (0) tip