--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 02 22:37:55 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 02 22:39:34 2014 +0100
@@ -325,7 +325,7 @@
ML_file "langford.ML"
method_setup dlo = {*
- Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+ Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
*} "Langford's algorithm for quantifier elimination in dense linear orders"
--- a/src/HOL/Decision_Procs/langford.ML Sun Mar 02 22:37:55 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Sun Mar 02 22:39:34 2014 +0100
@@ -2,13 +2,13 @@
Author: Amine Chaieb, TU Muenchen
*)
-signature LANGFORD_QE =
+signature LANGFORD =
sig
val dlo_tac : Proof.context -> int -> tactic
val dlo_conv : Proof.context -> cterm -> thm
end
-structure LangfordQE: LANGFORD_QE =
+structure Langford: LANGFORD =
struct
val dest_set =