--- a/src/HOL/ROOT.ML Mon Jul 19 15:24:35 1999 +0200 +++ b/src/HOL/ROOT.ML Mon Jul 19 15:27:34 1999 +0200 @@ -69,7 +69,7 @@ cd "Integ"; use_thy "IntDef"; use "simproc.ML"; -use_thy "IntDiv"; +use_thy "NatBin"; cd ".."; (*the all-in-one theory*)