doc-src/IsarAdvanced/Classes/classes.tex
changeset 28565 519b17118926
parent 28540 541366e3c1b3
child 28714 1992553cccfe
     1.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:23:33 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:52:45 2008 +0200
     1.3 @@ -3,71 +3,51 @@
     1.4  
     1.5  \documentclass[12pt,a4paper,fleqn]{report}
     1.6  \usepackage{latexsym,graphicx}
     1.7 -\usepackage{listings}
     1.8  \usepackage[refpage]{nomencl}
     1.9  \usepackage{../../iman,../../extra,../../isar,../../proof}
    1.10  \usepackage{../../isabelle,../../isabellesym}
    1.11  \usepackage{style}
    1.12  \usepackage{../../pdfsetup}
    1.13  
    1.14 -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
    1.15 -
    1.16 -\makeatletter
    1.17 -
    1.18 -\isakeeptag{quoteme}
    1.19 -\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    1.20 -\renewcommand{\isatagquoteme}{\begin{quoteme}}
    1.21 -\renewcommand{\endisatagquoteme}{\end{quoteme}}
    1.22 -
    1.23 -\makeatother
    1.24 -
    1.25 -\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    1.26 -\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    1.27 -\renewcommand{\isasymotimes}{\isamath{\circ}}
    1.28 -
    1.29 -\newcommand{\cmd}[1]{\isacommand{#1}}
    1.30  
    1.31 -\newcommand{\isasymINFIX}{\cmd{infix}}
    1.32 -\newcommand{\isasymLOCALE}{\cmd{locale}}
    1.33 -\newcommand{\isasymINCLUDES}{\cmd{includes}}
    1.34 -\newcommand{\isasymDATATYPE}{\cmd{datatype}}
    1.35 -\newcommand{\isasymAXCLASS}{\cmd{axclass}}
    1.36 -\newcommand{\isasymFIXES}{\cmd{fixes}}
    1.37 -\newcommand{\isasymASSUMES}{\cmd{assumes}}
    1.38 -\newcommand{\isasymDEFINES}{\cmd{defines}}
    1.39 -\newcommand{\isasymNOTES}{\cmd{notes}}
    1.40 -\newcommand{\isasymSHOWS}{\cmd{shows}}
    1.41 -\newcommand{\isasymCLASS}{\cmd{class}}
    1.42 -\newcommand{\isasymINSTANCE}{\cmd{instance}}
    1.43 -\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
    1.44 -\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
    1.45 -\newcommand{\isasymLEMMA}{\cmd{lemma}}
    1.46 -\newcommand{\isasymPROOF}{\cmd{proof}}
    1.47 -\newcommand{\isasymQED}{\cmd{qed}}
    1.48 -\newcommand{\isasymFIX}{\cmd{fix}}
    1.49 -\newcommand{\isasymASSUME}{\cmd{assume}}
    1.50 -\newcommand{\isasymSHOW}{\cmd{show}}
    1.51 -\newcommand{\isasymNOTE}{\cmd{note}}
    1.52 +%% setup
    1.53  
    1.54 -\newcommand{\qt}[1]{``#1''}
    1.55 -\newcommand{\qtt}[1]{"{}{#1}"{}}
    1.56 -\newcommand{\qn}[1]{\emph{#1}}
    1.57 -\newcommand{\strong}[1]{{\bfseries #1}}
    1.58 -\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
    1.59 -
    1.60 -\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
    1.61 -\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
    1.62 -\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
    1.63 -
    1.64 +% hyphenation
    1.65  \hyphenation{Isabelle}
    1.66  \hyphenation{Isar}
    1.67  
    1.68 +% logical markup
    1.69 +\newcommand{\strong}[1]{{\bfseries {#1}}}
    1.70 +\newcommand{\qn}[1]{\emph{#1}}
    1.71 +
    1.72 +% typographic conventions
    1.73 +\newcommand{\qt}[1]{``{#1}''}
    1.74 +
    1.75 +% verbatim text
    1.76 +\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
    1.77 +
    1.78 +% invisibility
    1.79  \isadroptag{theory}
    1.80 +
    1.81 +% quoted segments
    1.82 +\makeatletter
    1.83 +\isakeeptag{quote}
    1.84 +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    1.85 +\renewcommand{\isatagquote}{\begin{quotesegment}}
    1.86 +\renewcommand{\endisatagquote}{\end{quotesegment}}
    1.87 +\makeatother
    1.88 +
    1.89 +%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    1.90 +%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    1.91 +%\renewcommand{\isasymotimes}{\isamath{\circ}}
    1.92 +
    1.93 +
    1.94 +%% content
    1.95 +
    1.96  \title{\includegraphics[scale=0.5]{isabelle_isar}
    1.97    \\[4ex] Haskell-style type classes with Isabelle/Isar}
    1.98  \author{\emph{Florian Haftmann}}
    1.99  
   1.100 -
   1.101  \begin{document}
   1.102  
   1.103  \maketitle