author nipkow Fri, 30 Mar 2001 18:35:33 +0200 changeset 11238 1d789889c922 parent 11237 0ef5ecc1fd4d child 11239 be12c6f1ea75
*** empty log message ***
--- 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}}