moving Commutative_Ring to the correct theory
authorpaulson
Thu Sep 15 17:45:17 2005 +0200 (2005-09-15)
changeset 174210382f6877b98
parent 17420 bdcffa8d8665
child 17422 3b237822985d
moving Commutative_Ring to the correct theory
src/HOL/Main.thy
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/Main.thy	Thu Sep 15 17:44:53 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Sep 15 17:45:17 2005 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Commutative_Ring Refute Reconstruction
     1.8 +imports Refute Reconstruction 
     1.9 +        (*other theores need to be ancestors of Reconstruction, not Main!!*)
    1.10  
    1.11  begin
    1.12  
     2.1 --- a/src/HOL/Reconstruction.thy	Thu Sep 15 17:44:53 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Thu Sep 15 17:45:17 2005 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header{*Attributes for Reconstructing External Resolution Proofs*}
     2.5  
     2.6  theory Reconstruction
     2.7 -    imports Hilbert_Choice Map Infinite_Set Extraction
     2.8 +    imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
     2.9      uses "Tools/res_lib.ML"
    2.10  
    2.11  	 "Tools/res_clause.ML"