--- 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 =
--- 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 {*
--- 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
--- 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
--- 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 *}
--- 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"