1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Makefile Mon Jul 19 17:08:05 1999 +0200
1.3 @@ -0,0 +1,43 @@
1.4 +#
1.5 +# $Id$
1.6 +#
1.7 +
1.8 +## targets
1.9 +
1.10 +default: dvi
1.11 +
1.12 +
1.13 +## dependencies
1.14 +
1.15 +include ../Makefile.in
1.16 +
1.17 +NAME = isar-ref
1.18 +
1.19 +FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
1.20 + simplifier.tex classical.tex hol.tex \
1.21 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
1.22 +
1.23 +dvi: $(NAME).dvi
1.24 +
1.25 +$(NAME).dvi: $(FILES) isabelle_isar.eps
1.26 + touch $(NAME).ind
1.27 + $(LATEX) $(NAME)
1.28 + $(RAIL) $(NAME)
1.29 + $(BIBTEX) $(NAME)
1.30 + $(LATEX) $(NAME)
1.31 + $(LATEX) $(NAME)
1.32 + $(SEDINDEX) $(NAME)
1.33 + $(LATEX) $(NAME)
1.34 +
1.35 +pdf: $(NAME).pdf
1.36 +
1.37 +$(NAME).pdf: $(FILES) isabelle_isar.pdf
1.38 + touch $(NAME).ind
1.39 + $(PDFLATEX) $(NAME)
1.40 + $(RAIL) $(NAME)
1.41 + $(BIBTEX) $(NAME)
1.42 + $(PDFLATEX) $(NAME)
1.43 + $(PDFLATEX) $(NAME)
1.44 + $(SEDINDEX) $(NAME)
1.45 + $(FIXBOOKMARKS) $(NAME).out
1.46 + $(PDFLATEX) $(NAME)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/IsarRef/basics.tex Mon Jul 19 17:08:05 1999 +0200
2.3 @@ -0,0 +1,16 @@
2.4 +
2.5 +\chapter{Basic concepts}
2.6 +
2.7 +\section{Isabelle/Isar Theories}
2.8 +
2.9 +\section{The Isar proof language}
2.10 +
2.11 +\subsection{Proof methods}
2.12 +
2.13 +\subsection{Attributes}
2.14 +
2.15 +
2.16 +%%% Local Variables:
2.17 +%%% mode: latex
2.18 +%%% TeX-master: "isar-ref"
2.19 +%%% End:
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarRef/classical.tex Mon Jul 19 17:08:05 1999 +0200
3.3 @@ -0,0 +1,7 @@
3.4 +
3.5 +\chapter{The Classical Reasoner}
3.6 +
3.7 +%%% Local Variables:
3.8 +%%% mode: latex
3.9 +%%% TeX-master: "isar-ref"
3.10 +%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/IsarRef/hol.tex Mon Jul 19 17:08:05 1999 +0200
4.3 @@ -0,0 +1,7 @@
4.4 +
4.5 +\chapter{HOL specific elements}
4.6 +
4.7 +%%% Local Variables:
4.8 +%%% mode: latex
4.9 +%%% TeX-master: "isar-ref"
4.10 +%%% End:
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/intro.tex Mon Jul 19 17:08:05 1999 +0200
5.3 @@ -0,0 +1,7 @@
5.4 +
5.5 +\chapter{Introduction}
5.6 +
5.7 +%%% Local Variables:
5.8 +%%% mode: latex
5.9 +%%% TeX-master: "isar-ref"
5.10 +%%% End:
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Jul 19 17:08:05 1999 +0200
6.3 @@ -0,0 +1,61 @@
6.4 +
6.5 +%% $Id$
6.6 +
6.7 +\documentclass[12pt]{report}
6.8 +\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
6.9 +
6.10 +\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
6.11 +
6.12 +\author{\emph{Markus Wenzel} \\ TU M\"unchen}
6.13 +
6.14 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
6.15 +
6.16 +\pagestyle{headings}
6.17 +\sloppy
6.18 +\binperiod %%%treat . like a binary operator
6.19 +
6.20 +\railalias{lbrace}{\ttlbrace}
6.21 +\railalias{rbrace}{\ttrbrace}
6.22 +\railterm{lbrace,rbrace}
6.23 +
6.24 +\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
6.25 +
6.26 +
6.27 +\begin{document}
6.28 +
6.29 +\underscoreoff
6.30 +
6.31 +\maketitle
6.32 +
6.33 +\begin{abstract}
6.34 + FIXME
6.35 +\end{abstract}
6.36 +
6.37 +\pagenumbering{roman} \tableofcontents \clearfirst
6.38 +
6.39 +%FIXME
6.40 +\nocite{Rudnicki:1992:MizarOverview}
6.41 +\nocite{Harrison:1996:MizarHOL}
6.42 +\nocite{Rudnicki:1992:MizarOverview}
6.43 +\nocite{Trybulec:1993:MizarFeatures}
6.44 +\nocite{Syme:1997:DECLARE}
6.45 +\nocite{Syme:1998:thesis}
6.46 +\nocite{Syme:1999:TPHOL}
6.47 +\nocite{Wenzel:1999:TPHOL}
6.48 +
6.49 +\include{intro}
6.50 +\include{basics}
6.51 +\include{syntax}
6.52 +\include{pure}
6.53 +\include{simplifier}
6.54 +\include{classical}
6.55 +\include{hol}
6.56 +
6.57 +\begingroup
6.58 + \bibliographystyle{plain} \small\raggedright\frenchspacing
6.59 + \bibliography{../manual}
6.60 +\endgroup
6.61 +
6.62 +\input{isar-ref.ind}
6.63 +
6.64 +\end{document}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/IsarRef/pure.tex Mon Jul 19 17:08:05 1999 +0200
7.3 @@ -0,0 +1,7 @@
7.4 +
7.5 +\chapter{Common Isar elements}
7.6 +
7.7 +%%% Local Variables:
7.8 +%%% mode: latex
7.9 +%%% TeX-master: "isar-ref"
7.10 +%%% End:
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/IsarRef/simplifier.tex Mon Jul 19 17:08:05 1999 +0200
8.3 @@ -0,0 +1,7 @@
8.4 +
8.5 +\chapter{The Simplifier}
8.6 +
8.7 +%%% Local Variables:
8.8 +%%% mode: latex
8.9 +%%% TeX-master: "isar-ref"
8.10 +%%% End:
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/doc-src/IsarRef/syntax.tex Mon Jul 19 17:08:05 1999 +0200
9.3 @@ -0,0 +1,64 @@
9.4 +
9.5 +\chapter{Isar document syntax}
9.6 +
9.7 +\section{Inner versus outer syntax}
9.8 +
9.9 +\section{Lexical matters}
9.10 +
9.11 +\section{Common syntax entities}
9.12 +
9.13 +\subsection{Atoms}
9.14 +
9.15 +\begin{rail}
9.16 + name : ident | symident | string
9.17 + ;
9.18 +
9.19 + nameref : name | longident
9.20 + ;
9.21 +
9.22 + text : nameref | verbatim
9.23 + ;
9.24 +\end{rail}
9.25 +
9.26 +\subsection{Comments}
9.27 +
9.28 +\begin{rail}
9.29 + comment : (() | '--' text)
9.30 + ;
9.31 + interest : (() | '\%')
9.32 + ;
9.33 +\end{rail}
9.34 +
9.35 +
9.36 +\subsection{Sorts and arities}
9.37 +
9.38 +\begin{rail}
9.39 + sort : nameref | lbrace (nameref * ',') rbrace
9.40 + ;
9.41 + arity : ( () | '(' (sort + ',') ')' ) sort
9.42 + ;
9.43 + simple\-arity : ( () | '(' (sort + ',') ')' ) nameref
9.44 + ;
9.45 +\end{rail}
9.46 +
9.47 +
9.48 +\subsection{Terms and Types}
9.49 +
9.50 +\begin{rail}
9.51 +
9.52 +\end{rail}
9.53 +
9.54 +\subsection{Mixfix annotations}
9.55 +
9.56 +
9.57 +\subsection{}
9.58 +
9.59 +\subsection{}
9.60 +
9.61 +\subsection{}
9.62 +
9.63 +
9.64 +%%% Local Variables:
9.65 +%%% mode: latex
9.66 +%%% TeX-master: "isar-ref"
9.67 +%%% End: