tweaks to the documentation

--- 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: 

--- a/src/Doc/manual.bib	Mon Nov 25 14:50:31 2013 +0000
+++ b/src/Doc/manual.bib	Mon Nov 25 16:00:09 2013 +0000
@@ -194,7 +194,7 @@
 @incollection{basin91,
   author	= {David Basin and Matt Kaufmann},
   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
-		   Comparison}, 
+		   Comparison},
   crossref	= {huet-plotkin91},
   pages		= {89-119}}
 
@@ -472,7 +472,7 @@
 @book{constable86,
   author	= {R. L. Constable and others},
   title		= {Implementing Mathematics with the Nuprl Proof
-		 Development System}, 
+		 Development System},
   publisher	= Prentice,
   year		= 1986}
 
@@ -505,7 +505,7 @@
 @incollection{dybjer91,
   author	= {Peter Dybjer},
   title		= {Inductive Sets and Families in {Martin-L{\"o}f's} Type
-		  Theory and Their Set-Theoretic Semantics}, 
+		  Theory and Their Set-Theoretic Semantics},
   crossref	= {huet-plotkin91},
   pages		= {280-306}}
 
@@ -533,7 +533,7 @@
 @InProceedings{felty91a,
   Author	= {Amy Felty},
   Title		= {A Logic Program for Transforming Sequent Proofs to Natural
-		  Deduction Proofs}, 
+		  Deduction Proofs},
   crossref	= {extensions91},
   pages		= {157-178}}
 
@@ -566,9 +566,9 @@
 
 @inproceedings{OBJ,
   author	= {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
-		 and J. Meseguer}, 
+		 and J. Meseguer},
   title		= {Principles of {OBJ2}},
-  booktitle	= POPL, 
+  booktitle	= POPL,
   year		= 1985,
   pages		= {52-66}}
 
@@ -576,7 +576,7 @@
 
 @book{gallier86,
   author	= {J. H. Gallier},
-  title		= {Logic for Computer Science: 
+  title		= {Logic for Computer Science:
 		Foundations of Automatic Theorem Proving},
   year		= 1986,
   publisher	= {Harper \& Row}}
@@ -605,8 +605,8 @@
   author	= {Jean-Yves Girard},
   title		= {Proofs and Types},
   year		= 1989,
-  publisher	= CUP, 
-  note		= {Translated by Yves LaFont and Paul Taylor}}
+  publisher	= CUP,
+  note		= {Translated by Yves Lafont and Paul Taylor}}
 
 @Book{mgordon-hol,
   editor	= {M. J. C. Gordon and T. F. Melham},
@@ -777,21 +777,21 @@
 
 @article{huet78,
   author	= {G. P. Huet and B. Lang},
-  title		= {Proving and Applying Program Transformations Expressed with 
+  title		= {Proving and Applying Program Transformations Expressed with
 			Second-Order Patterns},
   journal	= acta,
   volume	= 11,
-  year		= 1978, 
+  year		= 1978,
   pages		= {31-55}}
 
 @inproceedings{huet88,
   author	= {G{\'e}rard Huet},
   title		= {Induction Principles Formalized in the {Calculus of
-		 Constructions}}, 
+		 Constructions}},
   booktitle	= {Programming of Future Generation Computers},
   editor	= {K. Fuchi and M. Nivat},
   year		= 1988,
-  pages		= {205-216}, 
+  pages		= {205-216},
   publisher	= {Elsevier}}
 
 @inproceedings{Huffman-Kuncar:2013:lifting_transfer,
@@ -843,7 +843,7 @@
 %K
 
 @InProceedings{kammueller-locales,
-  author = 	 {Florian Kamm{\"u}ller and Markus Wenzel and 
+  author = 	 {Florian Kamm{\"u}ller and Markus Wenzel and
                   Lawrence C. Paulson},
   title = 	 {Locales: A Sectioning Concept for {Isabelle}},
   crossref =	 {tphols99}}
@@ -944,7 +944,7 @@
   author	= {Gavin Lowe},
   title		= {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
 		  Protocol using {CSP} and {FDR}},
-  booktitle = 	 {Tools and Algorithms for the Construction and Analysis 
+  booktitle = 	 {Tools and Algorithms for the Construction and Analysis
                   of Systems:  second international workshop, TACAS '96},
   editor =	 {T. Margaria and B. Steffen},
   series =	 {LNCS 1055},
@@ -978,7 +978,7 @@
 @incollection{melham89,
   author	= {Thomas F. Melham},
   title		= {Automating Recursive Type Definitions in Higher Order
-		 Logic}, 
+		 Logic},
   pages		= {341-386},
   crossref	= {birtwistle89}}
 
@@ -1057,7 +1057,7 @@
 
 @InProceedings{NaraschewskiW-TPHOLs98,
   author	= {Wolfgang Naraschewski and Markus Wenzel},
-  title		= 
+  title		=
 {Object-Oriented Verification based on Record Subtyping in
                   Higher-Order Logic},
   crossref      = {tphols98}}
@@ -1190,8 +1190,8 @@
 @book{nordstrom90,
   author	= {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
   title		= {Programming in {Martin-L{\"o}f}'s Type Theory.  An
-		 Introduction}, 
-  publisher	= {Oxford University Press}, 
+		 Introduction},
+  publisher	= {Oxford University Press},
   year		= 1990}
 
 %O
@@ -1251,7 +1251,7 @@
 @InProceedings{paulson-COLOG,
   author	= {Lawrence C. Paulson},
   title		= {A Formulation of the Simple Theory of Types (for
-		 {Isabelle})}, 
+		 {Isabelle})},
   pages		= {246-274},
   crossref	= {colog88},
   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
@@ -1304,7 +1304,7 @@
 %replaces paulson-final
 @Article{paulson-mscs,
   author	= {Lawrence C. Paulson},
-  title = 	 {Final Coalgebras as Greatest Fixed Points 
+  title = 	 {Final Coalgebras as Greatest Fixed Points
                   in {ZF} Set Theory},
   journal	= {Mathematical Structures in Computer Science},
   year		= 1999,
@@ -1337,9 +1337,9 @@
   crossref	= {milner-fest}}
 
 @book{milner-fest,
-  title		= {Proof, Language, and Interaction: 
+  title		= {Proof, Language, and Interaction:
                    Essays in Honor of {Robin Milner}},
-  booktitle	= {Proof, Language, and Interaction: 
+  booktitle	= {Proof, Language, and Interaction:
                    Essays in Honor of {Robin Milner}},
   publisher	= MIT,
   year		= 2000,
@@ -1427,7 +1427,7 @@
 @book{paulson87,
   author	= {Lawrence C. Paulson},
   title		= {Logic and Computation: Interactive proof with Cambridge
-		 LCF}, 
+		 LCF},
   year		= 1987,
   publisher	= CUP}
 
@@ -1470,7 +1470,7 @@
 @article{pelletier86,
   author	= {F. J. Pelletier},
   title		= {Seventy-five Problems for Testing Automatic Theorem
-		 Provers}, 
+		 Provers},
   journal	= JAR,
   volume	= 2,
   pages		= {191-216},
@@ -1486,13 +1486,13 @@
   publisher	= CUP,
   year		= 1993}
 
-@Article{pitts94,  
+@Article{pitts94,
   author	= {Andrew M. Pitts},
   title		= {A Co-induction Principle for Recursively Defined Domains},
   journal	= TCS,
-  volume	= 124, 
+  volume	= 124,
   pages		= {195-219},
-  year		= 1994} 
+  year		= 1994}
 
 @Article{plaisted90,
   author	= {David A. Plaisted},
@@ -1561,7 +1561,7 @@
 @inproceedings{saaltink-fme,
   author	= {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
 		 Dan Craigen and Irwin Meisels},
-  title		= {An {EVES} Data Abstraction Example}, 
+  title		= {An {EVES} Data Abstraction Example},
   pages		= {578-596},
   crossref	= {fme93}}
 
@@ -1897,7 +1897,7 @@
   author	= {A. N. Whitehead and B. Russell},
   title		= {Principia Mathematica},
   year		= 1962,
-  publisher	= CUP, 
+  publisher	= CUP,
   note		= {Paperback edition to *56,
   abridged from the 2nd edition (1927)}}
 
@@ -1982,9 +1982,9 @@
 @book{birtwistle89,
   editor	= {Graham Birtwistle and P. A. Subrahmanyam},
   title		= {Current Trends in Hardware Verification and Automated
-		 Theorem Proving}, 
+		 Theorem Proving},
   booktitle	= {Current Trends in Hardware Verification and Automated
-		 Theorem Proving}, 
+		 Theorem Proving},
   publisher	= {Springer},
   year		= 1989}
 
@@ -1997,9 +1997,9 @@
 
 @Proceedings{cade12,
   editor	= {Alan Bundy},
-  title		= {Automated Deduction --- {CADE}-12 
+  title		= {Automated Deduction --- {CADE}-12
 		  International Conference},
-  booktitle	= {Automated Deduction --- {CADE}-12 
+  booktitle	= {Automated Deduction --- {CADE}-12
 		  International Conference},
   year		= 1994,
   series	= {LNAI 814},
@@ -2059,7 +2059,7 @@
   title		= {Extensions of Logic Programming},
   booktitle	= {Extensions of Logic Programming},
   year		= 1991,
-  series	= {LNAI 475}, 
+  series	= {LNAI 475},
   publisher	= {Springer}}
 
 @proceedings{cade10,
@@ -2078,9 +2078,9 @@
   year		= 1993}
 
 @book{wos-fest,
-  title		= {Automated Reasoning and its Applications: 
+  title		= {Automated Reasoning and its Applications:
 			Essays in Honor of {Larry Wos}},
-  booktitle	= {Automated Reasoning and its Applications: 
+  booktitle	= {Automated Reasoning and its Applications:
 			Essays in Honor of {Larry Wos}},
   publisher	= MIT,
   year		= 1997,