equal
deleted
inserted
replaced
1 header {* Various decision procedures, typically involving reflection *} |
1 header {* Various decision procedures, typically involving reflection *} |
2 |
2 |
3 theory Decision_Procs |
3 theory Decision_Procs |
4 imports |
4 imports |
5 Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order Parametric_Ferrante_Rackoff |
5 Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order |
|
6 Parametric_Ferrante_Rackoff |
6 Commutative_Ring_Complete |
7 Commutative_Ring_Complete |
7 "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" |
8 "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" |
8 begin |
9 begin |
9 |
10 |
10 end |
11 end |