author wenzelm Wed Mar 06 23:57:34 2002 +0100 (2002-03-06) changeset 13036 dca23533bdfb parent 13035 d3be9be2b307 child 13037 f7f29f8380ce
tuned;
     1.1 --- a/src/HOL/HoareParallel/document/root.tex	Wed Mar 06 18:16:48 2002 +0100
1.2 +++ b/src/HOL/HoareParallel/document/root.tex	Wed Mar 06 23:57:34 2002 +0100
1.3 @@ -22,6 +22,8 @@
1.4  \thispagestyle{empty}
1.5  \tableofcontents
1.6
1.7 +\clearpage
1.8 +
1.9  \begin{center}
1.10    \includegraphics[scale=0.7]{session_graph}
1.11  \end{center}

     2.1 --- a/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 18:16:48 2002 +0100
2.2 +++ b/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 23:57:34 2002 +0100
2.3 @@ -4,7 +4,7 @@
2.4      Copyright   2001  University of Cambridge
2.5  *)
2.6
2.7 -header {*  Square roots of primes are irrational (script version) *}
2.8 +header {* Square roots of primes are irrational (script version) *}
2.9
2.10  theory Sqrt_Script = Primes + Hyperreal:
2.11
2.12 @@ -18,7 +18,8 @@
2.13  lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p \<noteq> 0"
2.14    by (force simp add: prime_def)
2.15
2.16 -lemma prime_dvd_other_side: "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
2.17 +lemma prime_dvd_other_side:
2.18 +    "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
2.19    apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
2.20    apply (rule_tac j = "k * k" in dvd_mult_left, simp)
2.21    done
2.22 @@ -71,6 +72,7 @@
2.23      real_of_nat_mult [symmetric])
2.24    done
2.25
2.26 -lemmas two_sqrt_irrational = prime_sqrt_irrational [OF two_is_prime]
2.27 +lemmas two_sqrt_irrational =
2.28 +  prime_sqrt_irrational [OF two_is_prime]
2.29
2.30  end