diff -r c876bcb601fc -r 5b65449d7669 src/HOL/HoareParallel/RG_Com.thy
--- 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