diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/syntax.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/syntax.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,64 @@
+
+\chapter{Isar document syntax}
+
+\section{Inner versus outer syntax}
+
+\section{Lexical matters}
+
+\section{Common syntax entities}
+
+\subsection{Atoms}
+
+\begin{rail}
+  name : ident | symident | string
+  ;
+
+  nameref : name | longident
+  ;
+
+  text : nameref | verbatim
+  ;
+\end{rail}
+
+\subsection{Comments}
+
+\begin{rail}
+  comment : (() | '--' text)
+  ;
+  interest : (() | '\%')
+  ;
+\end{rail}
+
+
+\subsection{Sorts and arities}
+
+\begin{rail}
+  sort : nameref | lbrace (nameref * ',') rbrace
+  ;
+  arity : ( () | '(' (sort + ',') ')' ) sort
+  ;
+  simple\-arity : ( () | '(' (sort + ',') ')' ) nameref
+  ;
+\end{rail}
+
+
+\subsection{Terms and Types}
+
+\begin{rail}
+  
+\end{rail}
+
+\subsection{Mixfix annotations}
+
+
+\subsection{}
+
+\subsection{}
+
+\subsection{}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: