src/HOL/TLA/Init.thy
changeset 35318 e1b61c5fd494
parent 35108 e384e27c229f
child 42018 878f33040280
equal deleted inserted replaced
35317:d57da4abb47d 35318:e1b61c5fd494
    10 theory Init
    10 theory Init
    11 imports Action
    11 imports Action
    12 begin
    12 begin
    13 
    13 
    14 typedecl behavior
    14 typedecl behavior
    15 instance behavior :: world ..
    15 arities behavior :: world
    16 
    16 
    17 types
    17 types
    18   temporal = "behavior form"
    18   temporal = "behavior form"
    19 
    19 
    20 
    20