# HG changeset patch # User wenzelm # Date 1209739081 -7200 # Node ID 5b8382d495bed9ae6f0c4346a3a1031fbec5cebb # Parent 844068d16ba008d66edb1070339c7d15cbe0a8f6 added begin and imports; diff -r 844068d16ba0 -r 5b8382d495be doc-src/isar.sty --- a/doc-src/isar.sty Fri May 02 16:36:29 2008 +0200 +++ b/doc-src/isar.sty Fri May 02 16:38:01 2008 +0200 @@ -27,6 +27,8 @@ \newcommand{\isasymAND}{\isakeyword{and}} \newcommand{\isasymIS}{\isakeyword{is}} \newcommand{\isasymWHERE}{\isakeyword{where}} +\newcommand{\isasymBEGIN}{\isakeyword{begin}} +\newcommand{\isasymIMPORTS}{\isakeyword{imports}} \newcommand{\isarkeyword}[1]{{\mathord{\mathbf{#1}}}} \newcommand{\isarcmd}[1]{\isarkeyword{#1}}