no more shadowing of Min and Max by Approximation
authorimmler
Sat Feb 23 19:50:21 2019 +0000 (2 months ago ago)
changeset 7001154d19f1f0ba6
parent 70010 3bfa28b3a5b2
child 70015 58ef3b8a8460
child 70016 b1dfaa25130e
no more shadowing of Min and Max by Approximation
src/HOL/Decision_Procs/Approximation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 21 09:15:07 2019 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 19:50:21 2019 +0000
     1.3 @@ -1670,4 +1670,26 @@
     1.4  ML_file \<open>approximation_generator.ML\<close>
     1.5  setup "Approximation_Generator.setup"
     1.6  
     1.7 +section "Avoid pollution of name space"
     1.8 +
     1.9 +hide_const (open)
    1.10 +  Add
    1.11 +  Minus
    1.12 +  Mult
    1.13 +  Inverse
    1.14 +  Cos
    1.15 +  Arctan
    1.16 +  Abs
    1.17 +  Max
    1.18 +  Min
    1.19 +  Pi
    1.20 +  Sqrt
    1.21 +  Exp
    1.22 +  Powr
    1.23 +  Ln
    1.24 +  Power
    1.25 +  Floor
    1.26 +  Var
    1.27 +  Num
    1.28 +
    1.29  end