src/HOLCF/IOA/Storage/Action.thy
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