src/HOL/HoareParallel/RG_Com.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HoareParallel/RG_Com.thy	Tue Mar 05 17:11:25 2002 +0100
@@ -0,0 +1,25 @@
+
+header {* \chapter{The Rely-Guarantee Method} 
+
+\section {Abstract Syntax}
+*}
+
+theory RG_Com = Main:
+
+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