HOL/ex/ROOT.ML: only list BinEx once
authorhuffman
Wed, 21 Sep 2011 17:43:13 -0700
changeset 45038 e24bf05dd273
parent 45037 29b5ff81f709
child 45039 632a033616e9
HOL/ex/ROOT.ML: only list BinEx once
src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Sep 21 10:59:55 2011 -0700
+++ b/src/HOL/ex/ROOT.ML	Wed Sep 21 17:43:13 2011 -0700
@@ -54,7 +54,6 @@
   "Coherent",
   "PresburgerEx",
   "ReflectionEx",
-  "BinEx",
   "Sqrt",
   "Sqrt_Script",
   "Transfer_Ex",