changed imports due to new GCD.thy
authornipkow
Fri Jul 08 11:38:30 2005 +0200 (2005-07-08)
changeset 167605c5f051aaaaa
parent 16759 668e72b1c4d7
child 16761 99549528ce76
changed imports due to new GCD.thy
src/HOL/Finite_Set.thy
src/HOL/PreList.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jul 08 11:37:53 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jul 08 11:38:30 2005 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Divides Power Inductive Lattice_Locales
     1.8 +imports Power Inductive Lattice_Locales
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}
     2.1 --- a/src/HOL/PreList.thy	Fri Jul 08 11:37:53 2005 +0200
     2.2 +++ b/src/HOL/PreList.thy	Fri Jul 08 11:38:30 2005 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header{*A Basis for Building the Theory of Lists*}
     2.5  
     2.6  theory PreList
     2.7 -imports Wellfounded_Relations Presburger Recdef Relation_Power Parity
     2.8 +imports Wellfounded_Relations Presburger Relation_Power GCD
     2.9  begin
    2.10  
    2.11  text {*