src/HOL/Inductive.thy
author paulson
Wed, 15 Jul 1998 14:19:02 +0200
changeset 5148 74919e8f221c
parent 5105 0ff5bec04d02
child 6437 9bdfe07ba8e9
permissions -rw-r--r--
More tidying and removal of "\!\!... from Goal commands


Inductive = Gfp + Prod + Sum