Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
authorhaftmann
Thu Mar 11 14:39:58 2010 +0100 (2010-03-11)
changeset 357254d7e3cc9c52c
parent 35724 178ad68f93ed
child 35726 059d2f7b979f
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
src/HOL/Equiv_Relations.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Mar 11 14:38:20 2010 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Mar 11 14:39:58 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Equivalence Relations in Higher-Order Set Theory *}
     1.5  
     1.6  theory Equiv_Relations
     1.7 -imports Finite_Set Relation Plain
     1.8 +imports Big_Operators Relation Plain
     1.9  begin
    1.10  
    1.11  subsection {* Equivalence relations *}
     2.1 --- a/src/HOL/IsaMakefile	Thu Mar 11 14:38:20 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Thu Mar 11 14:39:58 2010 +0100
     2.3 @@ -142,7 +142,6 @@
     2.4  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
     2.5  
     2.6  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
     2.7 -  Big_Operators.thy \
     2.8    Complete_Lattice.thy \
     2.9    Datatype.thy \
    2.10    Extraction.thy \
    2.11 @@ -248,6 +247,7 @@
    2.12  
    2.13  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    2.14    ATP_Linkup.thy \
    2.15 +  Big_Operators.thy \
    2.16    Code_Evaluation.thy \
    2.17    Code_Numeral.thy \
    2.18    Divides.thy \