Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Dense_Linear_Order.thy
changeset 30738 0842e906300c
parent 30652 752329615264
child 30741 9e23e3ea7edd 
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
-imports Plain Groebner_Basis Main
+imports Main
 uses
   "~~/src/HOL/Tools/Qelim/langford_data.ML"
   "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
isabelle