# HG changeset patch
# User immler
# Date 1550955812 18000
# Node ID b1dfaa25130e3500146959f5df81beba46b91953
# Parent  54d19f1f0ba67c7604c8b0bd6f34005d130ef65c
bundles for floatarith notation

diff -r 54d19f1f0ba6 -r b1dfaa25130e src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 19:50:21 2019 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 16:03:32 2019 -0500
@@ -1672,6 +1672,52 @@
 
 section "Avoid pollution of name space"
 
+bundle floatarith_notation begin
+
+notation Add ("Add")
+notation Minus ("Minus")
+notation Mult ("Mult")
+notation Inverse ("Inverse")
+notation Cos ("Cos")
+notation Arctan ("Arctan")
+notation Abs ("Abs")
+notation Max ("Max")
+notation Min ("Min")
+notation Pi ("Pi")
+notation Sqrt ("Sqrt")
+notation Exp ("Exp")
+notation Powr ("Powr")
+notation Ln ("Ln")
+notation Power ("Power")
+notation Floor ("Floor")
+notation Var ("Var")
+notation Num ("Num")
+
+end
+
+bundle no_floatarith_notation begin
+
+no_notation Add ("Add")
+no_notation Minus ("Minus")
+no_notation Mult ("Mult")
+no_notation Inverse ("Inverse")
+no_notation Cos ("Cos")
+no_notation Arctan ("Arctan")
+no_notation Abs ("Abs")
+no_notation Max ("Max")
+no_notation Min ("Min")
+no_notation Pi ("Pi")
+no_notation Sqrt ("Sqrt")
+no_notation Exp ("Exp")
+no_notation Powr ("Powr")
+no_notation Ln ("Ln")
+no_notation Power ("Power")
+no_notation Floor ("Floor")
+no_notation Var ("Var")
+no_notation Num ("Num")
+
+end
+
 hide_const (open)
   Add
   Minus