tuned;
authorwenzelm
Wed Mar 06 23:57:34 2002 +0100 (2002-03-06)
changeset 13036dca23533bdfb
parent 13035 d3be9be2b307
child 13037 f7f29f8380ce
tuned;
src/HOL/HoareParallel/document/root.tex
src/HOL/Hyperreal/ex/Sqrt_Script.thy
     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