# HG changeset patch
# User haftmann
# Date 1268314798 -3600
# Node ID 4d7e3cc9c52c8a723bdea327fcde1269eb86de94
# Parent  178ad68f93edb6ce0aeffa653442bc87a9143cb4
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy

diff -r 178ad68f93ed -r 4d7e3cc9c52c src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Mar 11 14:38:20 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Mar 11 14:39:58 2010 +0100
@@ -5,7 +5,7 @@
 header {* Equivalence Relations in Higher-Order Set Theory *}
 
 theory Equiv_Relations
-imports Finite_Set Relation Plain
+imports Big_Operators Relation Plain
 begin
 
 subsection {* Equivalence relations *}
diff -r 178ad68f93ed -r 4d7e3cc9c52c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 11 14:38:20 2010 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 11 14:39:58 2010 +0100
@@ -142,7 +142,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
-  Big_Operators.thy \
   Complete_Lattice.thy \
   Datatype.thy \
   Extraction.thy \
@@ -248,6 +247,7 @@
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   ATP_Linkup.thy \
+  Big_Operators.thy \
   Code_Evaluation.thy \
   Code_Numeral.thy \
   Divides.thy \