src/HOL/Inductive.thy
author sandnerr
Mon, 09 Dec 1996 19:13:13 +0100
changeset 2355 ee9bdbe2ac8a
parent 1862 74d4ae2f6fc3
child 5102 8c782c25a11e
permissions -rw-r--r--
simpset extension moved from HOLCF.ML to One.ML and Tr2.ML

Inductive = Gfp + Prod + Sum + "indrule"