prefer main entry points of HOL;
authorwenzelm
Sat Nov 04 19:17:19 2017 +0100 (18 months ago)
changeset 67006b1278ed3cd46
parent 67005 11fca474d87a
child 67007 978c584609de
prefer main entry points of HOL;
src/HOL/Algebra/IntRing.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Cardinals/Order_Union.thy
src/HOL/Cardinals/Wellfounded_More.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Preorder.thy
src/HOL/Nonstandard_Analysis/HSEQ.thy
src/HOL/Nonstandard_Analysis/HTranscendental.thy
src/HOL/ex/Birthday_Paradox.thy
src/HOL/ex/Groebner_Examples.thy
src/HOL/ex/PresburgerEx.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Nov 04 18:57:49 2017 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Nov 04 19:17:19 2017 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  *)
     1.5  
     1.6  theory IntRing
     1.7 -imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int
     1.8 +imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
     1.9  begin
    1.10  
    1.11  section \<open>The Ring of Integers\<close>
     2.1 --- a/src/HOL/Analysis/L2_Norm.thy	Sat Nov 04 18:57:49 2017 +0100
     2.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Sat Nov 04 19:17:19 2017 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  section \<open>Square root of sum of squares\<close>
     2.5  
     2.6  theory L2_Norm
     2.7 -imports HOL.NthRoot
     2.8 +imports Complex_Main
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 18:57:49 2017 +0100
     3.2 +++ b/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 19:17:19 2017 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  section \<open>Order Union\<close>
     3.5  
     3.6  theory Order_Union
     3.7 -imports HOL.Order_Relation
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11  definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
     4.1 --- a/src/HOL/Cardinals/Wellfounded_More.thy	Sat Nov 04 18:57:49 2017 +0100
     4.2 +++ b/src/HOL/Cardinals/Wellfounded_More.thy	Sat Nov 04 19:17:19 2017 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  section \<open>More on Well-Founded Relations\<close>
     4.5  
     4.6  theory Wellfounded_More
     4.7 -imports HOL.Wellfounded Order_Relation_More
     4.8 +imports Main Order_Relation_More
     4.9  begin
    4.10  
    4.11  subsection \<open>Well-founded recursion via genuine fixpoints\<close>
     5.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Sat Nov 04 18:57:49 2017 +0100
     5.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Sat Nov 04 19:17:19 2017 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  section \<open>Type of (at Most) Countable Sets\<close>
     5.5  
     5.6  theory Countable_Set_Type
     5.7 -imports Countable_Set Cardinal_Notations HOL.Conditionally_Complete_Lattices
     5.8 +imports Countable_Set Cardinal_Notations
     5.9  begin
    5.10  
    5.11  
     6.1 --- a/src/HOL/Library/FuncSet.thy	Sat Nov 04 18:57:49 2017 +0100
     6.2 +++ b/src/HOL/Library/FuncSet.thy	Sat Nov 04 19:17:19 2017 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  section \<open>Pi and Function Sets\<close>
     6.5  
     6.6  theory FuncSet
     6.7 -  imports HOL.Hilbert_Choice Main
     6.8 +  imports Main
     6.9    abbrevs PiE = "Pi\<^sub>E"
    6.10      PIE = "\<Pi>\<^sub>E"
    6.11  begin
     7.1 --- a/src/HOL/Library/ListVector.thy	Sat Nov 04 18:57:49 2017 +0100
     7.2 +++ b/src/HOL/Library/ListVector.thy	Sat Nov 04 19:17:19 2017 +0100
     7.3 @@ -3,7 +3,7 @@
     7.4  section \<open>Lists as vectors\<close>
     7.5  
     7.6  theory ListVector
     7.7 -imports HOL.List Main
     7.8 +imports Main
     7.9  begin
    7.10  
    7.11  text\<open>\noindent
     8.1 --- a/src/HOL/Library/Option_ord.thy	Sat Nov 04 18:57:49 2017 +0100
     8.2 +++ b/src/HOL/Library/Option_ord.thy	Sat Nov 04 19:17:19 2017 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4  section \<open>Canonical order on option type\<close>
     8.5  
     8.6  theory Option_ord
     8.7 -imports HOL.Option Main
     8.8 +imports Main
     8.9  begin
    8.10  
    8.11  notation
     9.1 --- a/src/HOL/Library/Preorder.thy	Sat Nov 04 18:57:49 2017 +0100
     9.2 +++ b/src/HOL/Library/Preorder.thy	Sat Nov 04 19:17:19 2017 +0100
     9.3 @@ -3,7 +3,7 @@
     9.4  section \<open>Preorders with explicit equivalence relation\<close>
     9.5  
     9.6  theory Preorder
     9.7 -imports HOL.Orderings
     9.8 +imports Main
     9.9  begin
    9.10  
    9.11  class preorder_equiv = preorder
    10.1 --- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sat Nov 04 18:57:49 2017 +0100
    10.2 +++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sat Nov 04 19:17:19 2017 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4  section \<open>Sequences and Convergence (Nonstandard)\<close>
    10.5  
    10.6  theory HSEQ
    10.7 -  imports HOL.Limits NatStar
    10.8 +  imports Complex_Main NatStar
    10.9    abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
   10.10  begin
   10.11  
    11.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Nov 04 18:57:49 2017 +0100
    11.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Nov 04 19:17:19 2017 +0100
    11.3 @@ -8,7 +8,7 @@
    11.4  section\<open>Nonstandard Extensions of Transcendental Functions\<close>
    11.5  
    11.6  theory HTranscendental
    11.7 -imports HOL.Transcendental HSeries HDeriv
    11.8 +imports Complex_Main HSeries HDeriv
    11.9  begin
   11.10  
   11.11  definition
    12.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Sat Nov 04 18:57:49 2017 +0100
    12.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Sat Nov 04 19:17:19 2017 +0100
    12.3 @@ -5,7 +5,7 @@
    12.4  section \<open>A Formulation of the Birthday Paradox\<close>
    12.5  
    12.6  theory Birthday_Paradox
    12.7 -imports Main HOL.Binomial "HOL-Library.FuncSet"
    12.8 +imports Main "HOL-Library.FuncSet"
    12.9  begin
   12.10  
   12.11  section \<open>Cardinality\<close>
    13.1 --- a/src/HOL/ex/Groebner_Examples.thy	Sat Nov 04 18:57:49 2017 +0100
    13.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Sat Nov 04 19:17:19 2017 +0100
    13.3 @@ -5,7 +5,7 @@
    13.4  section \<open>Groebner Basis Examples\<close>
    13.5  
    13.6  theory Groebner_Examples
    13.7 -imports HOL.Groebner_Basis
    13.8 +imports Main
    13.9  begin
   13.10  
   13.11  subsection \<open>Basic examples\<close>
    14.1 --- a/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 18:57:49 2017 +0100
    14.2 +++ b/src/HOL/ex/PresburgerEx.thy	Sat Nov 04 19:17:19 2017 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  section \<open>Some examples for Presburger Arithmetic\<close>
    14.5  
    14.6  theory PresburgerEx
    14.7 -imports HOL.Presburger
    14.8 +imports Main
    14.9  begin
   14.10  
   14.11  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