--- a/src/HOL/HoareParallel/RG_Com.thy Thu Sep 17 14:17:37 2009 +1000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-
-header {* \chapter{The Rely-Guarantee Method}
-
-\section {Abstract Syntax}
-*}
-
-theory RG_Com imports Main begin
-
-text {* Semantics of assertions and boolean expressions (bexp) as sets
-of states. Syntax of commands @{text com} and parallel commands
-@{text par_com}. *}
-
-types
- 'a bexp = "'a set"
-
-datatype 'a com =
- Basic "'a \<Rightarrow>'a"
- | Seq "'a com" "'a com"
- | Cond "'a bexp" "'a com" "'a com"
- | While "'a bexp" "'a com"
- | Await "'a bexp" "'a com"
-
-types 'a par_com = "(('a com) option) list"
-
-end
\ No newline at end of file