author wenzelm Wed, 06 Mar 2002 23:57:34 +0100 changeset 13036 dca23533bdfb parent 13035 d3be9be2b307 child 13037 f7f29f8380ce
tuned;
--- 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}
--- 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 @@
*)

-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"

-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