src/HOL/Induct/Com.thy
changeset 16417 9bc16273c2d4
parent 14527 bc9e5587d05a
child 18260 5597cfcecd49
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     6 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     6 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     7 *)
     7 *)
     8 
     8 
     9 header{*Mutual Induction via Iteratived Inductive Definitions*}
     9 header{*Mutual Induction via Iteratived Inductive Definitions*}
    10 
    10 
    11 theory Com = Main:
    11 theory Com imports Main begin
    12 
    12 
    13 typedecl loc
    13 typedecl loc
    14 
    14 
    15 types  state = "loc => nat"
    15 types  state = "loc => nat"
    16        n2n2n = "nat => nat => nat"
    16        n2n2n = "nat => nat => nat"