src/HOL/Decision_Procs/Decision_Procs.thy
author haftmann
Mon Apr 26 15:37:50 2010 +0200 (2010-04-26)
changeset 36409 d323e7773aa8
parent 36347 0ca616bc6c6f
child 51544 8c58fbbc1d5a
permissions -rw-r--r--
use new classes (linordered_)field_inverse_zero
haftmann@33356
     1
header {* Various decision procedures, typically involving reflection *}
haftmann@30429
     2
haftmann@29825
     3
theory Decision_Procs
haftmann@33356
     4
imports
haftmann@35044
     5
  Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order
haftmann@35044
     6
  Parametric_Ferrante_Rackoff
haftmann@33356
     7
  Commutative_Ring_Complete
haftmann@33356
     8
  "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
haftmann@29825
     9
begin
haftmann@29825
    10
haftmann@36347
    11
end