src/HOL/Decision_Procs/Decision_Procs.thy
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 51544 8c58fbbc1d5a
child 58988 6ebf918128b9
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
haftmann@29825
     1
theory Decision_Procs
haftmann@33356
     2
imports
wenzelm@51544
     3
  Commutative_Ring
wenzelm@51544
     4
  Cooper
wenzelm@51544
     5
  Ferrack
wenzelm@51544
     6
  MIR
wenzelm@51544
     7
  Approximation
wenzelm@51544
     8
  Dense_Linear_Order
haftmann@35044
     9
  Parametric_Ferrante_Rackoff
haftmann@33356
    10
  Commutative_Ring_Complete
wenzelm@51544
    11
  "ex/Commutative_Ring_Ex"
wenzelm@51544
    12
  "ex/Approximation_Ex"
wenzelm@51544
    13
  "ex/Dense_Linear_Order_Ex"
haftmann@29825
    14
begin
haftmann@29825
    15
haftmann@36347
    16
end