# HG changeset patch
# User nipkow
# Date 1028130158 -7200
# Node ID 2f98365f57a84a90c85c0dc6da4c23cbd0836f5c
# Parent  527811f00c5689cea28be99ca58747ef66e0e091
*** empty log message ***

diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Datatype/Fundata.thy
--- a/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -40,8 +40,7 @@
 (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac T, rename_tac[2] F)(*>*)
 txt{*\noindent
-Because of the function type, the 
-the proof state after induction looks unusual.
+Because of the function type, the proof state after induction looks unusual.
 Notice the quantified induction hypothesis:
 @{subgoals[display,indent=0]}
 *}
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -51,8 +51,7 @@
 %
 \begin{isamarkuptxt}%
 \noindent
-Because of the function type, the 
-the proof state after induction looks unusual.
+Because of the function type, the proof state after induction looks unusual.
 Notice the quantified induction hypothesis:
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -118,7 +118,7 @@
   output as @{text "A\<^sup>\<star>"}.
 
   \medskip Replacing our definition of @{text xor} by the following
-  specifies a Isabelle symbol for the new operator:
+  specifies an Isabelle symbol for the new operator:
 *}
 
 (*<*)
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -122,7 +122,7 @@
   output as \isa{A\isactrlsup {\isasymstar}}.
 
   \medskip Replacing our definition of \isa{xor} by the following
-  specifies a Isabelle symbol for the new operator:%
+  specifies an Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/IsaMakefile
--- a/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 17:42:38 2002 +0200
@@ -14,7 +14,7 @@
 
 LNCS: $(LOG)/HOL-LNCS.gz
 
-$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/*.thy
+$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/document/root.bib LNCS/*.thy
 	@$(USEDIR) HOL LNCS
 
 
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/LNCS/FP0.thy
--- a/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -15,17 +15,6 @@
 "rev (x # xs)  = (rev xs) @ (x # [])"
 
 theorem rev_rev [simp]: "rev(rev xs) = xs"
-(*<*)oops(*>*)
+(*<*)oops(*>*)text_raw{*\isanewline\isanewline*}
 
-text{*
-\begin{exercise}
-Define a datatype of binary trees and a function @{term mirror}
-that mirrors a binary tree by swapping subtrees recursively. Prove
-@{prop"mirror(mirror t) = t"}.
-
-Define a function @{term flatten} that flattens a tree into a list
-by traversing it in infix order. Prove
-@{prop"flatten(mirror t) = rev(flatten t)"}.
-\end{exercise}
-*}
 end
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/LNCS/Ind.thy
--- a/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -61,11 +61,11 @@
 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
 inductive "r*"
 intros
-rtc_refl[iff]:  "(x,x) \<in> r*"
-rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+refl[iff]:  "(x,x) \<in> r*"
+step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
 
 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
-by(blast intro: rtc_step);
+by(blast intro: rtc.step);
 
 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
 apply(erule rtc.induct)
@@ -75,12 +75,12 @@
   "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
 apply(erule rtc.induct)
  apply(blast);
-apply(blast intro: rtc_step);
+apply(blast intro: rtc.step);
 done
 
 text{*
 \begin{exercise}
-Show that the converse of @{thm[source]rtc_step} also holds:
+Show that the converse of @{thm[source]rtc.step} also holds:
 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
 \end{exercise}*}
 
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/LNCS/document/root.bib
--- a/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 17:42:38 2002 +0200
@@ -3,4 +3,5 @@
 
 @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
-publisher=Springer,series=LNCS,volume=2283,year=2002}
+publisher=Springer,series=LNCS,volume=2283,year=2002,
+note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/LNCS/document/root.tex
--- a/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,8 @@
 \begin{document}
 
 \title{A Compact Overview of Isabelle/HOL}
-\author{Tobias Nipkow}
+\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
+ \small\url{http://www.in.tum.de/~nipkow/}}
 \date{}
 \maketitle
 
@@ -28,6 +29,16 @@
 \subsection{An Introductory Theory}
 \input{FP0.tex}
 
+\begin{exercise}
+Define a datatype of binary trees and a function \isa{mirror}
+that mirrors a binary tree by swapping subtrees recursively. Prove
+\isa{mirror(mirror t) = t}.
+
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+\isa{flatten(mirror t) = rev(flatten t)}.
+\end{exercise}
+
 \subsection{More Constructs}
 \input{FP1.tex}
 
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -4,7 +4,7 @@
  
 This chapter outlines the concepts and techniques that underlie reasoning
 in Isabelle.  Until now, we have proved everything using only induction and
-simplification, but any serious verification project require more elaborate
+simplification, but any serious verification project requires more elaborate
 forms of inference.  The chapter also introduces the fundamentals of
 predicate logic.  The first examples in this chapter will consist of
 detailed, low-level proof steps.  Later, we shall see how to automate such
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,7 @@
 function is a set, and the inverse image of a function maps sets to sets.
 
 This chapter will be useful to anybody who plans to develop a substantial
-proof.  sets are convenient for formalizing  computer science concepts such
+proof.  Sets are convenient for formalizing  computer science concepts such
 as grammars, logical calculi and state transition systems.  Isabelle can
 prove many statements involving sets automatically.
 
@@ -610,7 +610,7 @@
 general syntax for comprehension:
 \begin{isabelle}
 \isacommand{lemma}\ "f`A\ \isasymunion\ g`A\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\
-x\isacharbraceright)
+x\isacharbraceright)"
 \par\smallskip
 \isacommand{lemma}\ "f\ `\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\
 y\isacharbraceright"
diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -281,7 +281,7 @@
 variables are automatically renamed to avoid clashes with free variables. In
 addition, Isabelle has a third kind of variable, called a \textbf{schematic
   variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
-which must a~\isa{?} as its first character.  
+which must have a~\isa{?} as its first character.  
 Logically, an unknown is a free variable. But it may be
 instantiated by another term during the proof process. For example, the
 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},