# HG changeset patch
# User Christian Sternagel
# Date 1346299564 -32400
# Node ID 5cd8b4426a57dcbbfccd71ccb369dcf73b121955
# Parent  7a17ba4bc9974792f3f7e059a5a0cdb930b9e6de
Main is implicitly imported via Sublist

diff -r 7a17ba4bc997 -r 5cd8b4426a57 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 13:05:11 2012 +0900
+++ b/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 13:06:04 2012 +0900
@@ -6,9 +6,7 @@
 header {* Sublist Ordering *}
 
 theory Sublist_Order
-imports
-  Main
-  Sublist
+imports Sublist
 begin
 
 text {*