# 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 {*