# HG changeset patch
# User webertj
# Date 1236706758 0
# Node ID c132175cae7e0f070d46cfcd66df154da154b89c
# Parent  c41afa5607be35f22250b26f657942d535de10b9# Parent  9501af91c4a3510a53dcf9c4dc0ff4d5de32299b
Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

diff -r 9501af91c4a3 -r c132175cae7e doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Mar 10 17:39:06 2009 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Mar 10 17:39:18 2009 +0000
@@ -533,11 +533,11 @@
   Likewise, \verb!concl! may be used as a style to show just the
   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   \begin{center}
-    \isa{{\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   To print just the conclusion,
   \begin{center}
-    \isa{hd\ {\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   type
   \begin{quote}
diff -r 9501af91c4a3 -r c132175cae7e src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 10 17:39:06 2009 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 10 17:39:18 2009 +0000
@@ -2422,10 +2422,6 @@
 lemma "0 < (d :: int) \<Longrightarrow> 0 \<le> i mod d \<and> i mod d < d" by auto
 lemma "(d :: int) < 0 \<Longrightarrow> d < i mod d \<and> i mod d \<le> 0" by auto
 
-code_const "op div :: int \<Rightarrow> int \<Rightarrow> int" (SML "(fn i => fn d => if d = 0 then 0 else i div d)")
-code_const "op mod :: int \<Rightarrow> int \<Rightarrow> int" (SML "(fn i => fn d => if d = 0 then i else i mod d)")
-code_const "divmod :: int \<Rightarrow> int \<Rightarrow> (int * int)" (SML "(fn i => fn d => if d = 0 then (0, i) else IntInf.divMod (i, d))")
-
 ML {*
   val uneq_equations = PureThy.get_thms @{theory} "uneq_equations";
   val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
@@ -2448,7 +2444,7 @@
     fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
                    = @{term "Float"} $ to_int mantisse $ to_int exp
       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
-                   = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power_float (Float 5 1)"} $ to_nat exp)
+                   = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
                    = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
       | bot_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
@@ -2456,7 +2452,7 @@
     fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
                    = @{term "Float"} $ to_int mantisse $ to_int exp
       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
-                   = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power_float (Float 5 1)"} $ to_nat exp)
+                   = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
                    = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
       | top_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
diff -r 9501af91c4a3 -r c132175cae7e src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 17:39:06 2009 +0000
+++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 17:39:18 2009 +0000
@@ -9,7 +9,7 @@
 
 (* set *)
 translations
-  "xs" <= "set xs"
+  "xs" <= "CONST set xs"
 
 (* append *)
 syntax (latex output)
@@ -26,15 +26,15 @@
 
 (* Let *)
 translations 
-  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
-  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
+  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
 
   "_tuple_args x (_tuple_args y z)" ==
     "_tuple_args x (_tuple_arg (_tuple y z))"
 
-  "_bind (Some p) e" <= "_bind p (the e)"
-  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
-  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+  "_bind (Some p) e" <= "_bind p (CONST the e)"
+  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
+  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
 
 (* type constraints with spacing *)
 setup {*
diff -r 9501af91c4a3 -r c132175cae7e src/HOL/ex/ApproximationEx.thy
--- a/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 17:39:06 2009 +0000
+++ b/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 17:39:18 2009 +0000
@@ -3,7 +3,7 @@
 *)
 
 theory ApproximationEx
-imports "~~/src/HOL/Reflection/Approximation"
+imports "~~/src/HOL/Decision_Procs/Approximation"
 begin
 
 text {*
@@ -39,9 +39,14 @@
 lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
   by (approximation 10)
 
+lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+  by (approximation 20)
+
+lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+  by (approximation 10)
+
 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
   by (approximation 10)
 
-
 end