--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 22 22:55:41 2012 +0200
@@ -7,13 +7,11 @@
theory Dense_Linear_Order
imports Main
-uses
- "langford_data.ML"
- "ferrante_rackoff_data.ML"
- ("langford.ML")
- ("ferrante_rackoff.ML")
begin
+ML_file "langford_data.ML"
+ML_file "ferrante_rackoff_data.ML"
+
setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
context linorder
@@ -290,7 +288,7 @@
lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
-use "langford.ML"
+ML_file "langford.ML"
method_setup dlo = {*
Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
*} "Langford's algorithm for quantifier elimination in dense linear orders"
@@ -540,7 +538,7 @@
end
-use "ferrante_rackoff.ML"
+ML_file "ferrante_rackoff.ML"
method_setup ferrack = {*
Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)