src/HOL/Inductive.thy
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 1862 74d4ae2f6fc3
child 5102 8c782c25a11e
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson@1862
     1
Inductive = Gfp + Prod + Sum + "indrule"
lcp@1187
     2
paulson@1862
     3