src/ZF/inductive.thy
changeset 13895 b6105462ccd3
parent 13894 8018173a7979
child 13896 717bd79b976f
equal deleted inserted replaced
13894:8018173a7979 13895:b6105462ccd3
     1 (*Dummy theory to document dependencies *)
       
     2 
       
     3 inductive = "indrule"