# HG changeset patch
# User immler
# Date 1550951421 0
# Node ID 54d19f1f0ba67c7604c8b0bd6f34005d130ef65c
# Parent  3bfa28b3a5b24887f68754d0c1da8f8795580b1a
no more shadowing of Min and Max by Approximation

diff -r 3bfa28b3a5b2 -r 54d19f1f0ba6 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 21 09:15:07 2019 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 19:50:21 2019 +0000
@@ -1670,4 +1670,26 @@
 ML_file \<open>approximation_generator.ML\<close>
 setup "Approximation_Generator.setup"
 
+section "Avoid pollution of name space"
+
+hide_const (open)
+  Add
+  Minus
+  Mult
+  Inverse
+  Cos
+  Arctan
+  Abs
+  Max
+  Min
+  Pi
+  Sqrt
+  Exp
+  Powr
+  Ln
+  Power
+  Floor
+  Var
+  Num
+
 end