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 *}