src/HOL/Inductive.thy
author wenzelm
Fri Apr 16 14:48:16 1999 +0200 (1999-04-16)
changeset 6437 9bdfe07ba8e9
parent 5105 0ff5bec04d02
child 7357 d0e16da40ea2
permissions -rw-r--r--
'HOL/inductive' theory data;
     1 
     2 Inductive = Gfp + Prod + Sum +
     3 
     4 setup InductivePackage.setup
     5 
     6 end