# HG changeset patch
# User wenzelm
# Date 941216451 -7200
# Node ID 8005c92a85d7994b6eb6f2a6cc6f5bcd0ed57ebf
# Parent  3ee8ddca092d3ad0d2714f2893a7a793b4b5723c
tuned;

diff -r 3ee8ddca092d -r 8005c92a85d7 doc-src/IsarRef/refcard.tex
--- 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]
diff -r 3ee8ddca092d -r 8005c92a85d7 doc-src/iman.sty
--- 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
diff -r 3ee8ddca092d -r 8005c92a85d7 doc-src/isar.sty
--- 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{\}\}}}