--- a/src/Doc/Tutorial/document/rules.tex Mon Nov 25 14:50:31 2013 +0000
+++ b/src/Doc/Tutorial/document/rules.tex Mon Nov 25 16:00:09 2013 +0000
@@ -1,4 +1,4 @@
-%!TEX root = ../tutorial.tex
+%!TEX root = root.tex
\chapter{The Rules of the Game}
\label{chap:rules}
@@ -33,6 +33,8 @@
one symbol only. For predicate logic this can be
done, but when users define their own concepts they typically
have to refer to other symbols as well. It is best not to be dogmatic.
+Our system is not based on pure natural deduction, but includes elements from the sequent calculus
+and free-variable tableaux.
Natural deduction generally deserves its name. It is easy to use. Each
proof step consists of identifying the outermost symbol of a formula and
@@ -240,13 +242,14 @@
of a conjunction. Rules of this sort (where the conclusion is a subformula of a
premise) are called \textbf{destruction} rules because they take apart and destroy
a premise.%
-\footnote{This Isabelle terminology has no counterpart in standard logic texts,
+\footnote{This Isabelle terminology is not used in standard logic texts,
although the distinction between the two forms of elimination rule is well known.
Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote}
for example, writes ``The elimination rules
[for $\disj$ and $\exists$] are very
bad. What is catastrophic about them is the parasitic presence of a formula [$R$]
-which has no structural link with the formula which is eliminated.''}
+which has no structural link with the formula which is eliminated.''
+These Isabelle rules are inspired by the sequent calculus.}
The first proof step applies conjunction introduction, leaving
two subgoals: