src/HOL/Induct/Com.thy
changeset 12338 de0f4a63baa5
parent 11701 3d51fbf81c17
child 13075 d3e1d554cd6d
equal deleted inserted replaced
12337:7c6a970f0808 12338:de0f4a63baa5
    10 
    10 
    11 types loc
    11 types loc
    12       state = "loc => nat"
    12       state = "loc => nat"
    13       n2n2n = "nat => nat => nat"
    13       n2n2n = "nat => nat => nat"
    14 
    14 
    15 arities loc :: term
    15 arities loc :: type
    16 
    16 
    17 datatype
    17 datatype
    18   exp = N nat
    18   exp = N nat
    19       | X loc
    19       | X loc
    20       | Op n2n2n exp exp
    20       | Op n2n2n exp exp