doc-src/IsarRef/isar-ref.tex
changeset 7134 320b412e5800
parent 7050 c70d3402fef5
child 7135 8eabfd7e6b9b
     1.1 --- a/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 13:44:29 1999 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 14:59:32 1999 +0200
     1.3 @@ -1,14 +1,25 @@
     1.4  
     1.5  %% $Id$
     1.6  
     1.7 -\documentclass[12pt]{report}
     1.8 -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup}
     1.9 +\documentclass[12pt,fleqn]{report}
    1.10 +\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
    1.11  
    1.12  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    1.13  \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    1.14  
    1.15  \makeindex
    1.16  
    1.17 +\railterm{lbrace,rbrace,llbrace,rrbrace}
    1.18 +\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
    1.19 +
    1.20 +\railalias{name}{\railqtoken{name}}
    1.21 +\railalias{nameref}{\railqtoken{nameref}}
    1.22 +\railalias{text}{\railqtoken{text}}
    1.23 +\railalias{type}{\railqtoken{type}}
    1.24 +\railalias{term}{\railqtoken{term}}
    1.25 +\railalias{prop}{\railqtoken{prop}}
    1.26 +\railalias{atom}{\railqtoken{atom}}
    1.27 +
    1.28  
    1.29  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    1.30  
    1.31 @@ -16,20 +27,8 @@
    1.32  \sloppy
    1.33  \binperiod     %%%treat . like a binary operator
    1.34  
    1.35 -\railalias{lbrace}{\ttlbrace}
    1.36 -\railalias{rbrace}{\ttrbrace}
    1.37 -\railterm{lbrace,rbrace}
    1.38 -
    1.39 -\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
    1.40 -\railterm{name,nameref,text,type,term,prop,atom}
    1.41 +\renewcommand{\phi}{\varphi}
    1.42  
    1.43 -\makeatletter
    1.44 -\newcommand{\railtoken}[1]{{\rail@termfont{#1}}}
    1.45 -\newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}}
    1.46 -\makeatother
    1.47 -
    1.48 -\newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}}
    1.49 -\newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}}
    1.50  
    1.51  \begin{document}
    1.52  
    1.53 @@ -57,8 +56,7 @@
    1.54  \include{basics}
    1.55  \include{syntax}
    1.56  \include{pure}
    1.57 -\include{simplifier}
    1.58 -\include{classical}
    1.59 +\include{clasimp}
    1.60  \include{hol}
    1.61  
    1.62  \begingroup