# HG changeset patch
# User wenzelm
# Date 1362050664 -3600
# Node ID 6822aa82aafa5f9c4177ebd1fa4e84e1b303a5ba
# Parent  7cdb86c8eb30dc56949e5771ed930da87c955b72
simplified imports;

diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -6,7 +6,7 @@
 header {* Extended natural numbers (i.e. with infinity) *}
 
 theory Extended_Nat
-imports "~~/src/HOL/Main"
+imports Main
 begin
 
 class infinity =
diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -8,7 +8,7 @@
 header {* Extended real number line *}
 
 theory Extended_Real
-imports "~~/src/HOL/Complex_Main" Extended_Nat
+imports Complex_Main Extended_Nat
 begin
 
 text {*
diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -5,7 +5,7 @@
 header {* Frechet Derivative *}
 
 theory FrechetDeriv
-imports "~~/src/HOL/Complex_Main"
+imports Complex_Main
 begin
 
 definition
diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Library/Phantom_Type.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -4,7 +4,7 @@
 
 header {* A generic phantom type *}
 
-theory Phantom_Type imports "~~/src/HOL/Main" begin
+theory Phantom_Type imports Main begin
 
 datatype ('a, 'b) phantom = phantom 'b
 
diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Library/Product_plus.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -5,7 +5,7 @@
 header {* Additive group operations on product types *}
 
 theory Product_plus
-imports "~~/src/HOL/Main"
+imports Main
 begin
 
 subsection {* Operations *}
diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Thu Feb 28 12:09:32 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Thu Feb 28 12:24:24 2013 +0100
@@ -5,7 +5,7 @@
 header {* Useful Numerical Lemmas *}
 
 theory Misc_Numeric
-imports "~~/src/HOL/Main" "~~/src/HOL/Parity"
+imports Main Parity
 begin
 
 lemma the_elemI: "y = {x} ==> the_elem y = x"