diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/style.sty	Fri May 02 16:36:05 2008 +0200
@@ -36,9 +36,7 @@
 \newcommand{\isasymGUESS}{\isakeyword{guess}}
 \newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
 \newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
 \newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymBEGIN}{\isakeyword{begin}}
 \newcommand{\isasymEND}{\isakeyword{end}}
 \newcommand{\isasymCONSTS}{\isakeyword{consts}}
 \newcommand{\isasymDEFS}{\isakeyword{defs}}