# HG changeset patch # User paulson # Date 1119622861 -7200 # Node ID b74143e10410af78c2fd15f89e1b06517480577d # Parent 2bc33f0cfe9a9898399decdd1f1471bc199dc012 deleted a redundant "use" line diff -r 2bc33f0cfe9a -r b74143e10410 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Fri Jun 24 16:18:41 2005 +0200 +++ b/src/HOL/ROOT.ML Fri Jun 24 16:21:01 2005 +0200 @@ -23,7 +23,6 @@ use "~~/src/Provers/clasimp.ML"; use "~~/src/Provers/Arith/fast_lin_arith.ML"; use "~~/src/Provers/Arith/cancel_sums.ML"; -use "~~/src/Provers/Arith/abel_cancel.ML"; use "~~/src/Provers/Arith/assoc_fold.ML"; use "~~/src/Provers/quantifier1.ML"; use "~~/src/Provers/Arith/cancel_numerals.ML";