equal
deleted
inserted
replaced
1 (* Author: Johannes Hoelzl, TU Muenchen |
1 (* Author: Johannes Hoelzl, TU Muenchen |
2 Coercions removed by Dmitriy Traytel *) |
2 Coercions removed by Dmitriy Traytel *) |
3 |
3 |
4 header {* Prove Real Valued Inequalities by Computation *} |
4 header {* Prove Real Valued Inequalities by Computation *} |
5 |
5 |
6 theory Approximation_coercion |
6 theory Approximation |
7 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat |
7 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat |
8 begin |
8 begin |
9 |
9 |
10 declare [[coercion_map map]] |
10 declare [[coercion_map map]] |
11 declare [[coercion_map "% f g h . g o h o f"]] |
11 declare [[coercion_map "% f g h . g o h o f"]] |