# HG changeset patch
# User huffman
# Date 1316652193 25200
# Node ID e24bf05dd27309222e5aff5c4a146e9094e0e830
# Parent  29b5ff81f709a79f4049f539f4ff00cb02da9036
HOL/ex/ROOT.ML: only list BinEx once

diff -r 29b5ff81f709 -r e24bf05dd273 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",