header {* Various decision procedures. typically involving reflection *} theory Decision_Procs imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" begin end