--- a/doc-src/TutorialI/Overview/Isar.thy Fri Mar 30 18:18:22 2001 +0200
+++ b/doc-src/TutorialI/Overview/Isar.thy Fri Mar 30 18:35:33 2001 +0200
@@ -14,12 +14,14 @@
show "?toA \<subseteq> lfp ?F"
proof
fix s assume "s \<in> ?toA"
- then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast
+ then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A"
+ by blast
from stM show "s \<in> lfp ?F"
proof (rule converse_rtrancl_induct)
from tA have "t \<in> ?F (lfp ?F)" by blast
with mono_ef show "t \<in> lfp ?F" ..
- fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*" and "s' \<in> lfp ?F"
+ fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*"
+ and "s' \<in> lfp ?F"
then have "s \<in> ?F (lfp ?F)" by blast
with mono_ef show "s \<in> lfp ?F" ..
qed
--- a/doc-src/TutorialI/Overview/document/root.tex Fri Mar 30 18:18:22 2001 +0200
+++ b/doc-src/TutorialI/Overview/document/root.tex Fri Mar 30 18:35:33 2001 +0200
@@ -3,7 +3,7 @@
%for best-style documents ...
\urlstyle{rm}
-\isabellestyle{it}
+%\isabellestyle{it}
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}