# HG changeset patch
# User haftmann
# Date 1268314829 -3600
# Node ID 817b8e0f7086730928a0a36c43bc88df6b269a0a
# Parent  059d2f7b979f2fc396fd08dc0a7eb2dbfc824c56
Big_Operators now in Main rather than Plain

diff -r 059d2f7b979f -r 817b8e0f7086 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Mar 11 14:39:58 2010 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Mar 11 14:40:29 2010 +0100
@@ -8,7 +8,7 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded
-imports Transitive_Closure Big_Operators
+imports Transitive_Closure
 uses ("Tools/Function/size.ML")
 begin