src/HOL/Inductive.thy
changeset 5105 0ff5bec04d02
parent 5102 8c782c25a11e
child 6437 9bdfe07ba8e9
equal deleted inserted replaced
5104:230cca8452c7 5105:0ff5bec04d02
     1 Inductive = Gfp + Prod + Sum +
       
     2 
     1 
     3 end
     2 Inductive = Gfp + Prod + Sum
     4