# HG changeset patch
# User nipkow
# Date 985970133 -7200
# Node ID 1d789889c92297e536122bf9079f176a67bbabc0
# Parent  0ef5ecc1fd4d84f2dbe154081fbfbf0104bff5b1
*** empty log message ***

diff -r 0ef5ecc1fd4d -r 1d789889c922 doc-src/TutorialI/Overview/Isar.thy
--- 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
diff -r 0ef5ecc1fd4d -r 1d789889c922 doc-src/TutorialI/Overview/document/root.tex
--- 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}}