src/HOL/HOLCF/IOA/ex/TrivEx2.thy
changeset 58249 180f1b3508ed
parent 42151 4da4fc77664b
child 58310 91ea607a34d8
equal deleted inserted replaced
58248:25af24e1f37b 58249:180f1b3508ed
     6 
     6 
     7 theory TrivEx2
     7 theory TrivEx2
     8 imports IOA Abstraction
     8 imports IOA Abstraction
     9 begin
     9 begin
    10 
    10 
    11 datatype action = INC
    11 datatype_new 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