# HG changeset patch
# User chaieb
# Date 1097063888 -7200
# Node ID 96d5b6e2b6e4547a0d0070ab0fe208b024608d1f
# Parent  315079a40f31e5b96deea19e1777a234ddd2c565
changed in order to insert Barith.thy

diff -r 315079a40f31 -r 96d5b6e2b6e4 src/HOL/IsaMakefile
--- 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 \
diff -r 315079a40f31 -r 96d5b6e2b6e4 src/HOL/PreList.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 {*