src/HOL/HOLCF/IOA/ex/TrivEx.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58880 0baae4311a9f
equal deleted inserted replaced
58309:a09ec6daaa19 58310:91ea607a34d8
     6 
     6 
     7 theory TrivEx
     7 theory TrivEx
     8 imports Abstraction
     8 imports 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