# HG changeset patch
# User wenzelm
# Date 1466786174 -7200
# Node ID 7b23053be254c2eeda44a4916bbaa46673dc03a4
# Parent  6038ba2687cf1d0f5b86a5a35fe5cd0f7967d80b
misc tuning and modernization;

diff -r 6038ba2687cf -r 7b23053be254 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Jun 23 23:10:19 2016 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jun 24 18:36:14 2016 +0200
@@ -1,18 +1,24 @@
-(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
+(*  Title:      HOL/Library/Code_Real_Approx_By_Float.thy
+    Author:     Florian Haftmann
+    Author:     Johannes Hölzl
+    Author:     Tobias Nipkow
+*)
 
 theory Code_Real_Approx_By_Float
 imports Complex_Main Code_Target_Int
 begin
 
-text\<open>\textbf{WARNING} This theory implements mathematical reals by machine
-reals (floats). This is inconsistent. See the proof of False at the end of
-the theory, where an equality on mathematical reals is (incorrectly)
-disproved by mapping it to machine reals.
+text\<open>
+  \<^bold>\<open>WARNING!\<close> This theory implements mathematical reals by machine reals
+  (floats). This is inconsistent. See the proof of False at the end of the
+  theory, where an equality on mathematical reals is (incorrectly) disproved
+  by mapping it to machine reals.
 
-The value command cannot display real results yet.
+  The \<^theory_text>\<open>value\<close> command cannot display real results yet.
 
-The only legitimate use of this theory is as a tool for code generation
-purposes.\<close>
+  The only legitimate use of this theory is as a tool for code generation
+  purposes.
+\<close>
 
 code_printing
   type_constructor real \<rightharpoonup>
@@ -88,9 +94,10 @@
 context
 begin
 
-qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+qualified definition real_exp :: "real \<Rightarrow> real"
+  where "real_exp = exp"
 
-lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
+lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
   unfolding real_exp_def ..
 
 end
@@ -144,8 +151,8 @@
     and (OCaml) "Pervasives.asin"
 declare arcsin_def[code del]
 
-definition real_of_integer :: "integer \<Rightarrow> real" where
-  "real_of_integer = of_int \<circ> int_of_integer"
+definition real_of_integer :: "integer \<Rightarrow> real"
+  where "real_of_integer = of_int \<circ> int_of_integer"
 
 code_printing
   constant real_of_integer \<rightharpoonup>
@@ -155,27 +162,22 @@
 context
 begin
 
-qualified definition real_of_int :: "int \<Rightarrow> real" where
-  [code_abbrev]: "real_of_int = of_int"
+qualified definition real_of_int :: "int \<Rightarrow> real"
+  where [code_abbrev]: "real_of_int = of_int"
 
-lemma [code]:
-  "real_of_int = real_of_integer \<circ> integer_of_int"
+lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
 
-lemma [code_unfold del]:
-  "0 \<equiv> (of_rat 0 :: real)"
+lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
   by simp
 
-lemma [code_unfold del]:
-  "1 \<equiv> (of_rat 1 :: real)"
+lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
   by simp
 
-lemma [code_unfold del]:
-  "numeral k \<equiv> (of_rat (numeral k) :: real)"
+lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
   by simp
 
-lemma [code_unfold del]:
-  "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
+lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   by simp
 
 end
@@ -183,54 +185,43 @@
 code_printing
   constant Ratreal \<rightharpoonup> (SML)
 
-definition Realfract :: "int => int => real"
-where
-  "Realfract p q = of_int p / of_int q"
+definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
+  where "Realfract p q = of_int p / of_int q"
 
 code_datatype Realfract
 
 code_printing
   constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
 
-lemma [code]:
-  "Ratreal r = case_prod Realfract (quotient_of r)"
+lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
   by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
 
-lemma [code, code del]:
-  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
+lemma [code, code del]: "(HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool) = (HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool)"
   ..
 
-lemma [code, code del]:
-  "(plus :: real => real => real) = plus"
-  ..
-
-lemma [code, code del]:
-  "(uminus :: real => real) = uminus"
+lemma [code, code del]: "(plus :: real \<Rightarrow> real \<Rightarrow> real) = plus"
   ..
 
-lemma [code, code del]:
-  "(minus :: real => real => real) = minus"
+lemma [code, code del]: "(uminus :: real \<Rightarrow> real) = uminus"
   ..
 
-lemma [code, code del]:
-  "(times :: real => real => real) = times"
+lemma [code, code del]: "(minus :: real \<Rightarrow> real \<Rightarrow> real) = minus"
   ..
 
-lemma [code, code del]:
-  "(divide :: real => real => real) = divide"
+lemma [code, code del]: "(times :: real \<Rightarrow> real \<Rightarrow> real) = times"
   ..
 
-lemma [code]:
-  fixes r :: real
-  shows "inverse r = 1 / r"
+lemma [code, code del]: "(divide :: real \<Rightarrow> real \<Rightarrow> real) = divide"
+  ..
+
+lemma [code]: "inverse r = 1 / r" for r :: real
   by (fact inverse_eq_divide)
 
 notepad
 begin
   have "cos (pi/2) = 0" by (rule cos_pi_half)
   moreover have "cos (pi/2) \<noteq> 0" by eval
-  ultimately have "False" by blast
+  ultimately have False by blast
 end
 
 end
-