simplified imports;
authorwenzelm
Thu Feb 28 12:24:24 2013 +0100 (2013-02-28)
changeset 513016822aa82aafa
parent 51300 7cdb86c8eb30
child 51302 de47a499bc04
simplified imports;
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Phantom_Type.thy
src/HOL/Library/Product_plus.thy
src/HOL/Word/Misc_Numeric.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Feb 28 12:09:32 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Feb 28 12:24:24 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports "~~/src/HOL/Main"
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  class infinity =
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Feb 28 12:09:32 2013 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Feb 28 12:24:24 2013 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Extended real number line *}
     2.5  
     2.6  theory Extended_Real
     2.7 -imports "~~/src/HOL/Complex_Main" Extended_Nat
     2.8 +imports Complex_Main Extended_Nat
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Library/FrechetDeriv.thy	Thu Feb 28 12:09:32 2013 +0100
     3.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Thu Feb 28 12:24:24 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Frechet Derivative *}
     3.5  
     3.6  theory FrechetDeriv
     3.7 -imports "~~/src/HOL/Complex_Main"
     3.8 +imports Complex_Main
     3.9  begin
    3.10  
    3.11  definition
     4.1 --- a/src/HOL/Library/Phantom_Type.thy	Thu Feb 28 12:09:32 2013 +0100
     4.2 +++ b/src/HOL/Library/Phantom_Type.thy	Thu Feb 28 12:24:24 2013 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  
     4.5  header {* A generic phantom type *}
     4.6  
     4.7 -theory Phantom_Type imports "~~/src/HOL/Main" begin
     4.8 +theory Phantom_Type imports Main begin
     4.9  
    4.10  datatype ('a, 'b) phantom = phantom 'b
    4.11  
     5.1 --- a/src/HOL/Library/Product_plus.thy	Thu Feb 28 12:09:32 2013 +0100
     5.2 +++ b/src/HOL/Library/Product_plus.thy	Thu Feb 28 12:24:24 2013 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Additive group operations on product types *}
     5.5  
     5.6  theory Product_plus
     5.7 -imports "~~/src/HOL/Main"
     5.8 +imports Main
     5.9  begin
    5.10  
    5.11  subsection {* Operations *}
     6.1 --- a/src/HOL/Word/Misc_Numeric.thy	Thu Feb 28 12:09:32 2013 +0100
     6.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Thu Feb 28 12:24:24 2013 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Useful Numerical Lemmas *}
     6.5  
     6.6  theory Misc_Numeric
     6.7 -imports "~~/src/HOL/Main" "~~/src/HOL/Parity"
     6.8 +imports Main Parity
     6.9  begin
    6.10  
    6.11  lemma the_elemI: "y = {x} ==> the_elem y = x"