--- a/doc-src/IsarRef/refcard.tex Fri Oct 29 18:31:08 1999 +0200
+++ b/doc-src/IsarRef/refcard.tex Fri Oct 29 19:00:51 1999 +0200
@@ -77,14 +77,14 @@
\section{Proof methods}
\begin{tabular}{ll}
- \multicolumn{2}{l}{\textbf{Single rules (forward-chaining facts)}} \\[0.5ex]
+ \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
$assumption$ & apply assumption \\
$rule~a@1~\dots~a@n$ & apply some rule \\
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
$induct~x$ & apply induction rule \\
$contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
- \multicolumn{2}{l}{\textbf{Multiple rules (inserting facts)}} \\[0.5ex]
+ \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
$-$ & \text{no rules} \\
$intro~a@1~\dots~a@n$ & \text{introduction rules} \\
$elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex]
@@ -101,11 +101,11 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
- $RS~b$ & resolve fact with rule \\
$OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
$of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
+ $RS~b$ & resolve fact with rule \\
$standard$ & put into standard result form \\
- $rulify$ & put into standard object-rule form \\
+ $rulify$ & put into object-rule form \\
$elimify$ & put destruction rule into elimination form \\[1ex]
\multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
--- a/doc-src/iman.sty Fri Oct 29 18:31:08 1999 +0200
+++ b/doc-src/iman.sty Fri Oct 29 19:00:51 1999 +0200
@@ -113,6 +113,9 @@
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
\newcommand{\text}[1]{\mbox{#1}}
+\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
+\newcommand{\dsh}{\mathit{\dshsym}}
+
\let\int=\cap
\let\un=\cup
\let\inter=\bigcap
--- a/doc-src/isar.sty Fri Oct 29 18:31:08 1999 +0200
+++ b/doc-src/isar.sty Fri Oct 29 19:00:51 1999 +0200
@@ -70,7 +70,6 @@
\newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
\newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
\newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
-\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
\newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
\newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
\newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
@@ -80,10 +79,11 @@
\newcommand{\IS}[1]{(\ISNAME~#1)}
\newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
\newcommand{\LET}[1]{\LETNAME~#1}
-\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
\newcommand{\SUFF}[1]{\SUFFNAME~#1}
\newcommand{\ATT}[1]{\ap [#1]}
\newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
\newcommand{\ALSO}{\isarkeyword{also}}
\newcommand{\FINALLY}{\isarkeyword{finally}}
+\newcommand{\BG}{\isarkeyword{\{\{}}
+\newcommand{\EN}{\isarkeyword{\}\}}}