src/HOL/Decision_Procs/Decision_Procs.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 36347 0ca616bc6c6f
child 51544 8c58fbbc1d5a
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
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