src/HOL/Inductive.thy
changeset 6437 9bdfe07ba8e9
parent 5105 0ff5bec04d02
child 7357 d0e16da40ea2
equal deleted inserted replaced
6436:90eab99706e3 6437:9bdfe07ba8e9
     1 
     1 
     2 Inductive = Gfp + Prod + Sum
     2 Inductive = Gfp + Prod + Sum +
       
     3 
       
     4 setup InductivePackage.setup
       
     5 
       
     6 end