# HG changeset patch
# User wenzelm
# Date 1015455454 -3600
# Node ID dca23533bdfbd1f7c8ea77969f1e09da81e92b07
# Parent  d3be9be2b307f84b34e3f0774b86c46d4bfc08f0
tuned;

diff -r d3be9be2b307 -r dca23533bdfb src/HOL/HoareParallel/document/root.tex
--- a/src/HOL/HoareParallel/document/root.tex	Wed Mar 06 18:16:48 2002 +0100
+++ b/src/HOL/HoareParallel/document/root.tex	Wed Mar 06 23:57:34 2002 +0100
@@ -22,6 +22,8 @@
 \thispagestyle{empty}
 \tableofcontents
 
+\clearpage
+
 \begin{center}
   \includegraphics[scale=0.7]{session_graph}  
 \end{center}
diff -r d3be9be2b307 -r dca23533bdfb src/HOL/Hyperreal/ex/Sqrt_Script.thy
--- a/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 18:16:48 2002 +0100
+++ b/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 23:57:34 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2001  University of Cambridge
 *)
 
-header {*  Square roots of primes are irrational (script version) *}
+header {* Square roots of primes are irrational (script version) *}
 
 theory Sqrt_Script = Primes + Hyperreal:
 
@@ -18,7 +18,8 @@
 lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p \<noteq> 0"
   by (force simp add: prime_def)
 
-lemma prime_dvd_other_side: "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
+lemma prime_dvd_other_side:
+    "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
   apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
   apply (rule_tac j = "k * k" in dvd_mult_left, simp)
   done
@@ -71,6 +72,7 @@
     real_of_nat_mult [symmetric])
   done
 
-lemmas two_sqrt_irrational = prime_sqrt_irrational [OF two_is_prime]
+lemmas two_sqrt_irrational =
+  prime_sqrt_irrational [OF two_is_prime]
 
 end