author | haftmann |
Fri, 30 Oct 2009 13:59:49 +0100 | |
changeset 33356 | 9157d0f9f00e |
parent 33152 | 241cfaed158f |
child 35044 | 7c761a4bd91f |
permissions | -rw-r--r-- |
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33152
diff
changeset
|
1 |
header {* Various decision procedures, typically involving reflection *} |
30429
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
29825
diff
changeset
|
2 |
|
29825 | 3 |
theory Decision_Procs |
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33152
diff
changeset
|
4 |
imports |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33152
diff
changeset
|
5 |
Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order Parametric_Ferrante_Rackoff |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33152
diff
changeset
|
6 |
Commutative_Ring_Complete |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33152
diff
changeset
|
7 |
"ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" |
29825 | 8 |
begin |
9 |
||
10 |
end |