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