doc-src/Ref/theory-syntax.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/theory-syntax.tex	Mon Mar 21 10:51:28 1994 +0100
@@ -0,0 +1,83 @@
+%% $Id$
+
+\appendix
+\newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
+
+\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
+\begin{itemize}
+\item {\tt Typewriter font} denotes terminal symbols.
+\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
+  identifiers, type identifiers, natural numbers, \ML\ strings (with their
+  quotation marks) and arbitrary \ML\ text.  The first three are fully defined
+  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
+\end{itemize}
+
+\begin{rail}
+
+theoryDef : id '=' (name + '+') ('+' extension | ());
+
+name: id | string;
+
+extension : classes default types arities consts trans rules 'end' ml
+          ;
+
+classes : ()
+        | 'classes' ( ( id (  ()
+                            | '<' (id + ',')
+                           ) 
+                       ) + )
+        ;
+
+default : ()
+        | 'default' sort 
+        ;
+
+sort :  id
+     | '\{' (id * ',') '\}'
+     ;
+
+types :  ()
+      | 'types' ( ( type ( () | '(' infix ')' ) ) + )
+      ;
+
+type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );
+
+infix : ( 'infixr' | 'infixl' ) nat;
+
+
+arities :  ()
+        | 'arities' ((( name + ',' ) '::' arity ) + )
+        ;
+
+arity   : ( () 
+          | '(' (sort + ',') ')' 
+          ) id
+        ;
+
+
+consts :  ()
+       | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
+       ;
+
+constDecl : ( name + ',') '::' string ;
+
+
+mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
+       | infix
+       | 'binder' string nat ;
+
+trans : ()
+      | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
+      ;
+
+pat : ( () | ( '(' id ')' ) ) string;
+
+rules :  ()
+      | 'rules' (( id string ) + )
+      ;
+
+ml :  ()
+   | 'ML' text
+   ;
+
+\end{rail}