# HG changeset patch
# User wenzelm
# Date 1509819439 -3600
# Node ID b1278ed3cd463684c02de9373173ab028cb9b4d6
# Parent  11fca474d87aec207bd486d253cf2d05847473f9
prefer main entry points of HOL;

diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int
+imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
 begin
 
 section \<open>The Ring of Integers\<close>
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Square root of sum of squares\<close>
 
 theory L2_Norm
-imports HOL.NthRoot
+imports Complex_Main
 begin
 
 definition
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Cardinals/Order_Union.thy
--- a/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -7,7 +7,7 @@
 section \<open>Order Union\<close>
 
 theory Order_Union
-imports HOL.Order_Relation
+imports Main
 begin
 
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Cardinals/Wellfounded_More.thy
--- a/src/HOL/Cardinals/Wellfounded_More.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -8,7 +8,7 @@
 section \<open>More on Well-Founded Relations\<close>
 
 theory Wellfounded_More
-imports HOL.Wellfounded Order_Relation_More
+imports Main Order_Relation_More
 begin
 
 subsection \<open>Well-founded recursion via genuine fixpoints\<close>
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -9,7 +9,7 @@
 section \<open>Type of (at Most) Countable Sets\<close>
 
 theory Countable_Set_Type
-imports Countable_Set Cardinal_Notations HOL.Conditionally_Complete_Lattices
+imports Countable_Set Cardinal_Notations
 begin
 
 
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Library/FuncSet.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Pi and Function Sets\<close>
 
 theory FuncSet
-  imports HOL.Hilbert_Choice Main
+  imports Main
   abbrevs PiE = "Pi\<^sub>E"
     PIE = "\<Pi>\<^sub>E"
 begin
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Library/ListVector.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -3,7 +3,7 @@
 section \<open>Lists as vectors\<close>
 
 theory ListVector
-imports HOL.List Main
+imports Main
 begin
 
 text\<open>\noindent
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Library/Option_ord.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Canonical order on option type\<close>
 
 theory Option_ord
-imports HOL.Option Main
+imports Main
 begin
 
 notation
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Library/Preorder.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -3,7 +3,7 @@
 section \<open>Preorders with explicit equivalence relation\<close>
 
 theory Preorder
-imports HOL.Orderings
+imports Main
 begin
 
 class preorder_equiv = preorder
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Nonstandard_Analysis/HSEQ.thy
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -11,7 +11,7 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-  imports HOL.Limits NatStar
+  imports Complex_Main NatStar
   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -8,7 +8,7 @@
 section\<open>Nonstandard Extensions of Transcendental Functions\<close>
 
 theory HTranscendental
-imports HOL.Transcendental HSeries HDeriv
+imports Complex_Main HSeries HDeriv
 begin
 
 definition
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/ex/Birthday_Paradox.thy
--- a/src/HOL/ex/Birthday_Paradox.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/ex/Birthday_Paradox.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>A Formulation of the Birthday Paradox\<close>
 
 theory Birthday_Paradox
-imports Main HOL.Binomial "HOL-Library.FuncSet"
+imports Main "HOL-Library.FuncSet"
 begin
 
 section \<open>Cardinality\<close>
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Groebner Basis Examples\<close>
 
 theory Groebner_Examples
-imports HOL.Groebner_Basis
+imports Main
 begin
 
 subsection \<open>Basic examples\<close>
diff -r 11fca474d87a -r b1278ed3cd46 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Some examples for Presburger Arithmetic\<close>
 
 theory PresburgerEx
-imports HOL.Presburger
+imports Main
 begin
 
 lemma "\<And>m n ja ia. \<lbrakk>\<not> m \<le> j; \<not> (n::nat) \<le> i; (e::nat) \<noteq> 0; Suc j \<le> ja\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>ja ia. m \<le> ja \<longrightarrow> (if j = ja \<and> i = ia then e else 0) = 0" by presburger