author | wenzelm |
Sat, 23 Feb 2019 21:51:40 +0100 | |
changeset 69834 | 58ef3b8a8460 |
parent 69830 | 54d19f1f0ba6 (diff) |
parent 69833 | c3500cec8290 (current diff) |
child 69836 | 9b4901bda2a7 |
--- a/src/HOL/Decision_Procs/Approximation.thy Sat Feb 23 21:48:18 2019 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Feb 23 21:51:40 2019 +0100 @@ -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