src/ZF/Inductive.thy
changeset 12372 cd3a09c7dac9
parent 12208 5efe7b6874fd
child 13259 01fa0c8dbc92
equal deleted inserted replaced
12371:80ca9058db95 12372:cd3a09c7dac9
    16     "Tools/primrec_package.ML":
    16     "Tools/primrec_package.ML":
    17 
    17 
    18 setup IndCases.setup
    18 setup IndCases.setup
    19 setup DatatypeTactics.setup
    19 setup DatatypeTactics.setup
    20 
    20 
       
    21 
       
    22 (*belongs to theory ZF*)
       
    23 declare bspec [dest?]
       
    24 
       
    25 (*belongs to theory upair*)
       
    26 declare UnI1 [elim?]  UnI2 [elim?]
       
    27 
    21 end
    28 end