--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Jun 23 21:16:07 2013 +0200
@@ -14,61 +14,75 @@
The only legitimate use of this theory is as a tool for code generation
purposes. *}
-code_type real
- (SML "real")
- (OCaml "float")
+code_printing
+ type_constructor real \<rightharpoonup>
+ (SML) "real"
+ and (OCaml) "float"
-code_const Ratreal
- (SML "error/ \"Bad constant: Ratreal\"")
+code_printing
+ constant Ratreal \<rightharpoonup>
+ (SML) "error/ \"Bad constant: Ratreal\""
-code_const "0 :: real"
- (SML "0.0")
- (OCaml "0.0")
+code_printing
+ constant "0 :: real" \<rightharpoonup>
+ (SML) "0.0"
+ and (OCaml) "0.0"
declare zero_real_code[code_unfold del]
-code_const "1 :: real"
- (SML "1.0")
- (OCaml "1.0")
+code_printing
+ constant "1 :: real" \<rightharpoonup>
+ (SML) "1.0"
+ and (OCaml) "1.0"
declare one_real_code[code_unfold del]
-code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.== ((_), (_))")
- (OCaml "Pervasives.(=)")
+code_printing
+ constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.== ((_), (_))"
+ and (OCaml) "Pervasives.(=)"
-code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.<= ((_), (_))")
- (OCaml "Pervasives.(<=)")
+code_printing
+ constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.<= ((_), (_))"
+ and (OCaml) "Pervasives.(<=)"
-code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.< ((_), (_))")
- (OCaml "Pervasives.(<)")
+code_printing
+ constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.< ((_), (_))"
+ and (OCaml) "Pervasives.(<)"
-code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.+ ((_), (_))")
- (OCaml "Pervasives.( +. )")
+code_printing
+ constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.+ ((_), (_))"
+ and (OCaml) "Pervasives.( +. )"
-code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.* ((_), (_))")
- (OCaml "Pervasives.( *. )")
+code_printing
+ constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.* ((_), (_))"
+ and (OCaml) "Pervasives.( *. )"
-code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.- ((_), (_))")
- (OCaml "Pervasives.( -. )")
+code_printing
+ constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.- ((_), (_))"
+ and (OCaml) "Pervasives.( -. )"
-code_const "uminus :: real \<Rightarrow> real"
- (SML "Real.~")
- (OCaml "Pervasives.( ~-. )")
+code_printing
+ constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.~"
+ and (OCaml) "Pervasives.( ~-. )"
-code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.'/ ((_), (_))")
- (OCaml "Pervasives.( '/. )")
+code_printing
+ constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.'/ ((_), (_))"
+ and (OCaml) "Pervasives.( '/. )"
-code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.== ((_:real), (_))")
+code_printing
+ constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.== ((_:real), (_))"
-code_const "sqrt :: real \<Rightarrow> real"
- (SML "Math.sqrt")
- (OCaml "Pervasives.sqrt")
+code_printing
+ constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Math.sqrt"
+ and (OCaml) "Pervasives.sqrt"
declare sqrt_def[code del]
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
@@ -76,55 +90,64 @@
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
unfolding real_exp_def ..
-code_const real_exp
- (SML "Math.exp")
- (OCaml "Pervasives.exp")
+code_printing
+ constant real_exp \<rightharpoonup>
+ (SML) "Math.exp"
+ and (OCaml) "Pervasives.exp"
declare real_exp_def[code del]
declare exp_def[code del]
hide_const (open) real_exp
-code_const ln
- (SML "Math.ln")
- (OCaml "Pervasives.ln")
+code_printing
+ constant ln \<rightharpoonup>
+ (SML) "Math.ln"
+ and (OCaml) "Pervasives.ln"
declare ln_def[code del]
-code_const cos
- (SML "Math.cos")
- (OCaml "Pervasives.cos")
+code_printing
+ constant cos \<rightharpoonup>
+ (SML) "Math.cos"
+ and (OCaml) "Pervasives.cos"
declare cos_def[code del]
-code_const sin
- (SML "Math.sin")
- (OCaml "Pervasives.sin")
+code_printing
+ constant sin \<rightharpoonup>
+ (SML) "Math.sin"
+ and (OCaml) "Pervasives.sin"
declare sin_def[code del]
-code_const pi
- (SML "Math.pi")
- (OCaml "Pervasives.pi")
+code_printing
+ constant pi \<rightharpoonup>
+ (SML) "Math.pi"
+ and (OCaml) "Pervasives.pi"
declare pi_def[code del]
-code_const arctan
- (SML "Math.atan")
- (OCaml "Pervasives.atan")
+code_printing
+ constant arctan \<rightharpoonup>
+ (SML) "Math.atan"
+ and (OCaml) "Pervasives.atan"
declare arctan_def[code del]
-code_const arccos
- (SML "Math.scos")
- (OCaml "Pervasives.acos")
+code_printing
+ constant arccos \<rightharpoonup>
+ (SML) "Math.scos"
+ and (OCaml) "Pervasives.acos"
declare arccos_def[code del]
-code_const arcsin
- (SML "Math.asin")
- (OCaml "Pervasives.asin")
+code_printing
+ constant arcsin \<rightharpoonup>
+ (SML) "Math.asin"
+ 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"
-code_const real_of_integer
- (SML "Real.fromInt")
- (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
+code_printing
+ constant real_of_integer \<rightharpoonup>
+ (SML) "Real.fromInt"
+ and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
definition real_of_int :: "int \<Rightarrow> real" where
[code_abbrev]: "real_of_int = of_int"
@@ -151,7 +174,8 @@
hide_const (open) real_of_int
-code_const Ratreal (SML)
+code_printing
+ constant Ratreal \<rightharpoonup> (SML)
definition Realfract :: "int => int => real"
where
@@ -159,8 +183,8 @@
code_datatype Realfract
-code_const Realfract
- (SML "Real.fromInt _/ '// Real.fromInt _")
+code_printing
+ constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
lemma [code]:
"Ratreal r = split Realfract (quotient_of r)"