# HG changeset patch # User nipkow # Date 990197155 -7200 # Node ID b28bbb153603378a9b506cb321780c2f5077d277 # Parent 891fbd3f48813d2beb83404687c999103ad92ce4 *** empty log message *** diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Advanced/WFrec.thy --- a/doc-src/TutorialI/Advanced/WFrec.thy Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri May 18 16:45:55 2001 +0200 @@ -37,7 +37,7 @@ example, @{term"measure f"} is always well-founded, and the lexicographic product of two well-founded relations is again well-founded, which we relied on when defining Ackermann's function above. -Of course the lexicographic product can also be interated: +Of course the lexicographic product can also be iterated: *} consts contrived :: "nat \ nat \ nat \ nat" diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 16:45:55 2001 +0200 @@ -39,7 +39,7 @@ example, \isa{measure\ f} is always well-founded, and the lexicographic product of two well-founded relations is again well-founded, which we relied on when defining Ackermann's function above. -Of course the lexicographic product can also be interated:% +Of course the lexicographic product can also be iterated:% \end{isamarkuptext}% \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ contrived\isanewline diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri May 18 16:45:55 2001 +0200 @@ -102,8 +102,9 @@ intermediate value theorem @{thm[source]nat0_intermed_int_val} @{thm[display]nat0_intermed_int_val[no_vars]} where @{term f} is of type @{typ"nat \ int"}, @{typ int} are the integers, -@{text"\.\"} is the absolute value function, and @{term"#1::int"} is the -integer 1 (see \S\ref{sec:numbers}). +@{text"\.\"} is the absolute value function\footnote{See +Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} +syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}). First we show that our specific function, the difference between the numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/Star.thy --- a/doc-src/TutorialI/Inductive/Star.thy Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Inductive/Star.thy Fri May 18 16:45:55 2001 +0200 @@ -36,7 +36,7 @@ the standard definition. We start with a simple lemma: *} -lemma [intro]: "(x,y) : r \ (x,y) \ r*" +lemma [intro]: "(x,y) \ r \ (x,y) \ r*" by(blast intro: rtc_step); text{*\noindent diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 16:45:55 2001 +0200 @@ -98,8 +98,9 @@ \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% \end{isabelle} where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, -\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the -integer 1 (see \S\ref{sec:numbers}). +\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See +Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} +syntax.}, and \isa{{\isacharhash}{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}). First we show that our specific function, the difference between the numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri May 18 16:45:55 2001 +0200 @@ -38,7 +38,7 @@ The rest of this section is devoted to proving that it is equivalent to the standard definition. We start with a simple lemma:% \end{isamarkuptext}% -\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline +\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}% \begin{isamarkuptext}% \noindent diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Types/Typedef.thy --- a/doc-src/TutorialI/Types/Typedef.thy Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Types/Typedef.thy Fri May 18 16:45:55 2001 +0200 @@ -200,7 +200,7 @@ @{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the representation: *} -lemma cases_lemma: "\ Q 0; Q 1; Q 2; n : three \ \ Q n"; +lemma cases_lemma: "\ Q 0; Q 1; Q 2; n \ three \ \ Q n"; txt{*\noindent Expanding @{thm[source]three_def} yields the premise @{prop"n\2"}. Repeated diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Types/document/Typedef.tex --- a/doc-src/TutorialI/Types/document/Typedef.tex Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri May 18 16:45:55 2001 +0200 @@ -199,7 +199,7 @@ \isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the representation:% \end{isamarkuptext}% -\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharcolon}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}% +\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}% \begin{isamarkuptxt}% \noindent Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated