1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Sat Nov 27 16:08:10 2010 -0800
1.3 @@ -0,0 +1,16 @@
1.4 +(* Title: HOLCF/IOA/ABP/Action.thy
1.5 + Author: Olaf Müller
1.6 +*)
1.7 +
1.8 +header {* The set of all actions of the system *}
1.9 +
1.10 +theory Action
1.11 +imports Main
1.12 +begin
1.13 +
1.14 +datatype action = New | Loc nat | Free nat
1.15 +
1.16 +lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
1.17 + by simp
1.18 +
1.19 +end