# HG changeset patch
# User wenzelm
# Date 932396885 -7200
# Node ID 9f755ff43cff17ceab2989b42e0f9399a1f588cb
# Parent  d6595926aa106cba2319426b5d58e3dfa52d49c7
skeleton only;

diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Makefile	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,43 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../Makefile.in
+
+NAME = isar-ref
+
+FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
+	simplifier.tex classical.tex hol.tex \
+	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+	touch $(NAME).ind
+	$(LATEX) $(NAME)
+	$(RAIL) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
+	touch $(NAME).ind
+	$(PDFLATEX) $(NAME)
+	$(RAIL) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/basics.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/basics.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,16 @@
+
+\chapter{Basic concepts}
+
+\section{Isabelle/Isar Theories}
+
+\section{The Isar proof language}
+
+\subsection{Proof methods}
+
+\subsection{Attributes}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/classical.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/classical.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,7 @@
+
+\chapter{The Classical Reasoner}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/hol.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/hol.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,7 @@
+
+\chapter{HOL specific elements}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/intro.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/intro.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,7 @@
+
+\chapter{Introduction}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/isar-ref.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,61 @@
+
+%% $Id$
+
+\documentclass[12pt]{report}
+\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
+
+\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
+
+\author{\emph{Markus Wenzel} \\ TU M\"unchen}
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod     %%%treat . like a binary operator
+
+\railalias{lbrace}{\ttlbrace}
+\railalias{rbrace}{\ttrbrace}
+\railterm{lbrace,rbrace}
+
+\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
+
+
+\begin{document}
+
+\underscoreoff
+
+\maketitle 
+
+\begin{abstract}
+  FIXME
+\end{abstract}
+
+\pagenumbering{roman} \tableofcontents \clearfirst
+
+%FIXME
+\nocite{Rudnicki:1992:MizarOverview}
+\nocite{Harrison:1996:MizarHOL}
+\nocite{Rudnicki:1992:MizarOverview}
+\nocite{Trybulec:1993:MizarFeatures}
+\nocite{Syme:1997:DECLARE}
+\nocite{Syme:1998:thesis}
+\nocite{Syme:1999:TPHOL}
+\nocite{Wenzel:1999:TPHOL}
+
+\include{intro}
+\include{basics}
+\include{syntax}
+\include{pure}
+\include{simplifier}
+\include{classical}
+\include{hol}
+
+\begingroup
+  \bibliographystyle{plain} \small\raggedright\frenchspacing
+  \bibliography{../manual}
+\endgroup
+
+\input{isar-ref.ind}
+
+\end{document}
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/pure.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/pure.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,7 @@
+
+\chapter{Common Isar elements}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
diff -r d6595926aa10 -r 9f755ff43cff doc-src/IsarRef/simplifier.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/simplifier.tex	Mon Jul 19 17:08:05 1999 +0200
@@ -0,0 +1,7 @@
+
+\chapter{The Simplifier}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: 
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: