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