| changeset 16417 | 9bc16273c2d4 | 
| parent 16298 | 8435be7188cb | 
| child 16733 | 236dfafbeb63 | 
--- a/src/HOL/HoareParallel/OG_Examples.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/HoareParallel/OG_Examples.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,7 +1,7 @@ header {* \section{Examples} *} -theory OG_Examples = OG_Syntax: +theory OG_Examples imports OG_Syntax begin subsection {* Mutual Exclusion *}