src/HOL/Inductive.thy
changeset 5102 8c782c25a11e
parent 1862 74d4ae2f6fc3
child 5105 0ff5bec04d02
equal deleted inserted replaced
5101:52e7c75acfe6 5102:8c782c25a11e
     1 Inductive = Gfp + Prod + Sum + "indrule"
     1 Inductive = Gfp + Prod + Sum +
     2 
     2 
       
     3 end
     3 
     4