src/ZF/Datatype.thy
changeset 124 858ab9a9b047
child 516 1957113f0d7d
equal deleted inserted replaced
123:0a2f744e008a 124:858ab9a9b047
       
     1 (*Dummy theory to document dependencies *)
       
     2 
       
     3 Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
       
     4                (*this must be capital to avoid conflicts with ML's "datatype" *)