src/HOL/HOLCF/IOA/ex/TrivEx2.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58880 0baae4311a9f
equal deleted inserted replaced
58309:a09ec6daaa19 58310:91ea607a34d8
     6 
     6 
     7 theory TrivEx2
     7 theory TrivEx2
     8 imports IOA Abstraction
     8 imports IOA Abstraction
     9 begin
     9 begin
    10 
    10 
    11 datatype_new action = INC
    11 datatype action = INC
    12 
    12 
    13 definition
    13 definition
    14   C_asig :: "action signature" where
    14   C_asig :: "action signature" where
    15   "C_asig = ({},{INC},{})"
    15   "C_asig = ({},{INC},{})"
    16 definition
    16 definition