src/HOL/Inductive.thy
author paulson
Wed, 25 Nov 1998 15:54:41 +0100
changeset 5971 c5a7a7685826
parent 5105 0ff5bec04d02
child 6437 9bdfe07ba8e9
permissions -rw-r--r--
simplified ensures_UNIV


Inductive = Gfp + Prod + Sum