skeleton only;
authorwenzelm
Mon Jul 19 17:08:05 1999 +0200 (1999-07-19)
changeset 70469f755ff43cff
parent 7045 d6595926aa10
child 7047 d103b875ef1d
skeleton only;
doc-src/IsarRef/Makefile
doc-src/IsarRef/basics.tex
doc-src/IsarRef/classical.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/intro.tex
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/simplifier.tex
doc-src/IsarRef/syntax.tex
     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: