# HG changeset patch
# User nipkow
# Date 971882364 -7200
# Node ID f11d37d4472de0eae29f598feadc18b78fbb9165
# Parent  028f54cd2cc9691ff5a25a2062c2a1f457b0109c
*** empty log message ***

diff -r 028f54cd2cc9 -r f11d37d4472d doc-src/TutorialI/Inductive/Star.thy
--- a/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:18 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:24 2000 +0200
@@ -3,6 +3,7 @@
 section{*The reflexive transitive closure*}
 
 text{*\label{sec:rtc}
+
 {\bf Say something about inductive relations as opposed to sets? Or has that
 been said already? If not, explain induction!}
 
@@ -24,9 +25,9 @@
 The function @{term rtc} is annotated with concrete syntax: instead of
 @{text"rtc r"} we can read and write {term"r*"}. The actual definition
 consists of two rules. Reflexivity is obvious and is immediately declared an
-equivalence rule.  Thus the automatic tools will apply it automatically. The
-second rule, @{thm[source]rtc_step}, says that we can always add one more
-@{term r}-step to the left. Although we could make @{thm[source]rtc_step} an
+equivalence.  Thus the automatic tools will apply it automatically. The second
+rule, @{thm[source]rtc_step}, says that we can always add one more @{term
+r}-step to the left. Although we could make @{thm[source]rtc_step} an
 introduction rule, this is dangerous: the recursion slows down and may
 even kill the automatic tactics.
 
diff -r 028f54cd2cc9 -r f11d37d4472d doc-src/TutorialI/Inductive/document/Star.tex
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:18 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:24 2000 +0200
@@ -6,6 +6,7 @@
 %
 \begin{isamarkuptext}%
 \label{sec:rtc}
+
 {\bf Say something about inductive relations as opposed to sets? Or has that
 been said already? If not, explain induction!}
 
@@ -13,7 +14,7 @@
 closure of a relation. This concept was already introduced in
 \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
 the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
+fixpoint because at that point in the theory hierarchy
 inductive definitions are not yet available. But now they are:%
 \end{isamarkuptext}%
 \isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
@@ -26,9 +27,8 @@
 The function \isa{rtc} is annotated with concrete syntax: instead of
 \isa{rtc\ r} we can read and write {term"r*"}. The actual definition
 consists of two rules. Reflexivity is obvious and is immediately declared an
-equivalence rule.  Thus the automatic tools will apply it automatically. The
-second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
-\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
+equivalence.  Thus the automatic tools will apply it automatically. The second
+rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
 introduction rule, this is dangerous: the recursion slows down and may
 even kill the automatic tactics.