1.1 --- a/doc-src/IsarRef/refcard.tex	Fri Oct 29 18:31:08 1999 +0200
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Fri Oct 29 19:00:51 1999 +0200
     1.3 @@ -77,14 +77,14 @@
     1.4  \section{Proof methods}
     1.5  
     1.6  \begin{tabular}{ll}
     1.7 -  \multicolumn{2}{l}{\textbf{Single rules (forward-chaining facts)}} \\[0.5ex]
     1.8 +  \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
     1.9    $assumption$ & apply assumption \\
    1.10    $rule~a@1~\dots~a@n$ & apply some rule  \\
    1.11    $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    1.12    $induct~x$ & apply induction rule \\
    1.13    $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
    1.14  
    1.15 -  \multicolumn{2}{l}{\textbf{Multiple rules (inserting facts)}} \\[0.5ex]
    1.16 +  \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
    1.17    $-$ & \text{no rules} \\
    1.18    $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
    1.19    $elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex]
    1.20 @@ -101,11 +101,11 @@
    1.21  
    1.22  \begin{tabular}{ll}
    1.23    \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
    1.24 -  $RS~b$ & resolve fact with rule \\
    1.25    $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
    1.26    $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
    1.27 +  $RS~b$ & resolve fact with rule \\
    1.28    $standard$ & put into standard result form \\
    1.29 -  $rulify$ & put into standard object-rule form \\
    1.30 +  $rulify$ & put into object-rule form \\
    1.31    $elimify$ & put destruction rule into elimination form \\[1ex]
    1.32  
    1.33    \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]

     2.1 --- a/doc-src/iman.sty	Fri Oct 29 18:31:08 1999 +0200
     2.2 +++ b/doc-src/iman.sty	Fri Oct 29 19:00:51 1999 +0200
     2.3 @@ -113,6 +113,9 @@
     2.4  \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
     2.5  \newcommand{\text}[1]{\mbox{#1}}
     2.6  
     2.7 +\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
     2.8 +\newcommand{\dsh}{\mathit{\dshsym}}
     2.9 +
    2.10  \let\int=\cap
    2.11  \let\un=\cup
    2.12  \let\inter=\bigcap

     3.1 --- a/doc-src/isar.sty	Fri Oct 29 18:31:08 1999 +0200
     3.2 +++ b/doc-src/isar.sty	Fri Oct 29 19:00:51 1999 +0200
     3.3 @@ -70,7 +70,6 @@
     3.4  \newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
     3.5  \newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
     3.6  \newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
     3.7 -\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
     3.8  \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
     3.9  \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
    3.10  \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
    3.11 @@ -80,10 +79,11 @@
    3.12  \newcommand{\IS}[1]{(\ISNAME~#1)}
    3.13  \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
    3.14  \newcommand{\LET}[1]{\LETNAME~#1}
    3.15 -\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
    3.16  \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    3.17  \newcommand{\SUFF}[1]{\SUFFNAME~#1}
    3.18  \newcommand{\ATT}[1]{\ap [#1]}
    3.19  \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
    3.20  \newcommand{\ALSO}{\isarkeyword{also}}
    3.21  \newcommand{\FINALLY}{\isarkeyword{finally}}
    3.22 +\newcommand{\BG}{\isarkeyword{\{\{}}
    3.23 +\newcommand{\EN}{\isarkeyword{\}\}}}