1354 RealArith.gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) |
1354 RealArith.gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) |
1355 end; |
1355 end; |
1356 |
1356 |
1357 val known_sos_constants = |
1357 val known_sos_constants = |
1358 [@{term "op ==>"}, @{term "Trueprop"}, |
1358 [@{term "op ==>"}, @{term "Trueprop"}, |
1359 @{term "op -->"}, @{term "op &"}, @{term "op |"}, |
1359 @{term HOL.implies}, @{term "op &"}, @{term "op |"}, |
1360 @{term "Not"}, @{term "op = :: bool => _"}, |
1360 @{term "Not"}, @{term "op = :: bool => _"}, |
1361 @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, |
1361 @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, |
1362 @{term "op = :: real => _"}, @{term "op < :: real => _"}, |
1362 @{term "op = :: real => _"}, @{term "op < :: real => _"}, |
1363 @{term "op <= :: real => _"}, |
1363 @{term "op <= :: real => _"}, |
1364 @{term "op + :: real => _"}, @{term "op - :: real => _"}, |
1364 @{term "op + :: real => _"}, @{term "op - :: real => _"}, |