# HG changeset patch
# User nipkow
# Date 1120815510 -7200
# Node ID 5c5f051aaaaa54ea3ef1731e5fcbfd214eaf6974
# Parent  668e72b1c4d7267ba5c1dab7fc5a5c8e295e2b1d
changed imports due to new GCD.thy

diff -r 668e72b1c4d7 -r 5c5f051aaaaa src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jul 08 11:37:53 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jul 08 11:38:30 2005 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Divides Power Inductive Lattice_Locales
+imports Power Inductive Lattice_Locales
 begin
 
 subsection {* Definition and basic properties *}
diff -r 668e72b1c4d7 -r 5c5f051aaaaa src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Fri Jul 08 11:37:53 2005 +0200
+++ b/src/HOL/PreList.thy	Fri Jul 08 11:38:30 2005 +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 Presburger Relation_Power GCD
 begin
 
 text {*