| changeset 13022 | b115b305612f |
| parent 13020 | 791e3b4c4039 |
| child 15425 | 6356d2523f73 |
--- a/src/HOL/HoareParallel/OG_Syntax.thy Tue Mar 05 17:14:11 2002 +0100 +++ b/src/HOL/HoareParallel/OG_Syntax.thy Tue Mar 05 18:19:11 2002 +0100 @@ -1,7 +1,5 @@ -header {* \section{Concrete Syntax} *} - -theory OG_Syntax = Quote_Antiquote + OG_Tactics: +theory OG_Syntax = OG_Tactics + Quote_Antiquote: text{* Syntax for commands and for assertions and boolean expressions in commands @{text com} and annotated commands @{text ann_com}. *}