changeset 40774 | 0437dbc127b3 |
parent 40773 | 6c12f5e24e34 |
child 40775 | ed7a4eadb2f6 |
--- a/src/HOLCF/IOA/Storage/Action.thy Sat Nov 27 14:34:54 2010 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Title: HOLCF/IOA/ABP/Action.thy - Author: Olaf Müller -*) - -header {* The set of all actions of the system *} - -theory Action -imports Main -begin - -datatype action = New | Loc nat | Free nat - -lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y" - by simp - -end