--- a/src/HOL/IsaMakefile Tue Oct 05 15:40:26 2004 +0200
+++ b/src/HOL/IsaMakefile Wed Oct 06 13:58:08 2004 +0200
@@ -85,6 +85,7 @@
Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
+ Integ/barith.ML Integ/Barith.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
--- a/src/HOL/PreList.thy Tue Oct 05 15:40:26 2004 +0200
+++ b/src/HOL/PreList.thy Wed Oct 06 13:58:08 2004 +0200
@@ -7,7 +7,7 @@
header{*A Basis for Building the Theory of Lists*}
theory PreList
-imports Wellfounded_Relations Presburger Recdef Relation_Power Parity
+imports Wellfounded_Relations Barith Recdef Relation_Power Parity
begin
text {*