--- 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]}
*}
--- 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
--- 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:
*}
(*<*)
--- 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%
--- 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
--- 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
--- 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}*}
--- 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/}}}
--- 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}
--- 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
--- 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"
--- 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},