src/HOL/While.ML
Wed, 30 Aug 2000 16:29:21 +0200 nipkow introduced induct_thm_tac
Wed, 26 Jul 2000 19:43:28 +0200 nipkow While functional for defining tail-recursive functions
less more (0) tip