src/HOL/HoareParallel/RG_Syntax.thy

--- a/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -1,7 +1,5 @@
 
-header {* \section{Concrete Syntax} *}
-
-theory RG_Syntax = Quote_Antiquote + RG_Hoare:
+theory RG_Syntax = RG_Hoare + Quote_Antiquote:
 
 syntax
   "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)