--- a/src/HOL/Decision_Procs/Decision_Procs.thy Fri Oct 23 10:11:56 2009 +0200
+++ b/src/HOL/Decision_Procs/Decision_Procs.thy Sun Oct 25 08:57:35 2009 +0100
@@ -1,7 +1,7 @@
header {* Various decision procedures. typically involving reflection *}
theory Decision_Procs
-imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
+imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" Parametric_Ferrante_Rackoff
begin
end
\ No newline at end of file