src/HOL/Inductive.thy
author berghofe
Tue Jun 30 20:51:15 1998 +0200 (1998-06-30)
changeset 5102 8c782c25a11e
parent 1862 74d4ae2f6fc3
child 5105 0ff5bec04d02
permissions -rw-r--r--
Adapted to new inductive definition package.
     1 Inductive = Gfp + Prod + Sum +
     2 
     3 end
     4