Main is implicitly imported via Sublist
authorChristian Sternagel
Thu, 30 Aug 2012 13:06:04 +0900
changeset 49088 5cd8b4426a57
parent 49087 7a17ba4bc997
child 49089 cd73b439cbe5
Main is implicitly imported via Sublist
src/HOL/Library/Sublist.thy
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 {*