1(*  Title:      HOL/HOLCF/IOA/Storage/Action.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The set of all actions of the system\<close>
6
7theory Action
8imports Main
9begin
10
11datatype action = New | Loc nat | Free nat
12
13lemma [cong]: "\<And>x. x = y \<Longrightarrow> case_action a b c x = case_action a b c y"
14  by simp
15
16end
17