--- /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)
--- /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:
--- /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:
--- /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:
--- /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:
--- /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}
--- /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:
--- /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:
--- /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: