# HG changeset patch # User wenzelm # Date 1550955100 -3600 # Node ID 58ef3b8a84600dd1b17733921b0f2a0aaed2f81d # Parent 54d19f1f0ba67c7604c8b0bd6f34005d130ef65c# Parent c3500cec829001b31cde37843577edd0974455a3 merged diff -r c3500cec8290 -r 58ef3b8a8460 src/HOL/Decision_Procs/Approximation.thy --- 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 \approximation_generator.ML\ 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