1 (* Title: HOLCF/IOA/ABP/Action.thy
2 Author: Olaf Müller
3 *)
4
5 header {* The set of all actions of the system *}
6
7 theory Action
8 imports Main
9 begin
10
11 datatype action = New | Loc nat | Free nat
12
13 lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
14 by simp
15
16 end