bundles for floatarith notation
authorimmler
Sat Feb 23 16:03:32 2019 -0500 (8 weeks ago ago)
changeset 70016b1dfaa25130e
parent 70011 54d19f1f0ba6
child 70017 9b4901bda2a7
bundles for floatarith notation
src/HOL/Decision_Procs/Approximation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 19:50:21 2019 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Feb 23 16:03:32 2019 -0500
     1.3 @@ -1672,6 +1672,52 @@
     1.4  
     1.5  section "Avoid pollution of name space"
     1.6  
     1.7 +bundle floatarith_notation begin
     1.8 +
     1.9 +notation Add ("Add")
    1.10 +notation Minus ("Minus")
    1.11 +notation Mult ("Mult")
    1.12 +notation Inverse ("Inverse")
    1.13 +notation Cos ("Cos")
    1.14 +notation Arctan ("Arctan")
    1.15 +notation Abs ("Abs")
    1.16 +notation Max ("Max")
    1.17 +notation Min ("Min")
    1.18 +notation Pi ("Pi")
    1.19 +notation Sqrt ("Sqrt")
    1.20 +notation Exp ("Exp")
    1.21 +notation Powr ("Powr")
    1.22 +notation Ln ("Ln")
    1.23 +notation Power ("Power")
    1.24 +notation Floor ("Floor")
    1.25 +notation Var ("Var")
    1.26 +notation Num ("Num")
    1.27 +
    1.28 +end
    1.29 +
    1.30 +bundle no_floatarith_notation begin
    1.31 +
    1.32 +no_notation Add ("Add")
    1.33 +no_notation Minus ("Minus")
    1.34 +no_notation Mult ("Mult")
    1.35 +no_notation Inverse ("Inverse")
    1.36 +no_notation Cos ("Cos")
    1.37 +no_notation Arctan ("Arctan")
    1.38 +no_notation Abs ("Abs")
    1.39 +no_notation Max ("Max")
    1.40 +no_notation Min ("Min")
    1.41 +no_notation Pi ("Pi")
    1.42 +no_notation Sqrt ("Sqrt")
    1.43 +no_notation Exp ("Exp")
    1.44 +no_notation Powr ("Powr")
    1.45 +no_notation Ln ("Ln")
    1.46 +no_notation Power ("Power")
    1.47 +no_notation Floor ("Floor")
    1.48 +no_notation Var ("Var")
    1.49 +no_notation Num ("Num")
    1.50 +
    1.51 +end
    1.52 +
    1.53  hide_const (open)
    1.54    Add
    1.55    Minus