--- a/src/HOL/Library/Quickcheck_Types.thy Thu Jul 24 14:04:55 2014 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Thu Jul 24 14:08:29 2014 +0200
@@ -4,7 +4,7 @@
*)
theory Quickcheck_Types
-imports "../Main"
+imports Main
begin
text {*
--- a/src/HOL/Quickcheck_Examples/Completeness.thy Thu Jul 24 14:04:55 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy Thu Jul 24 14:08:29 2014 +0200
@@ -6,7 +6,7 @@
header {* Proving completeness of exhaustive generators *}
theory Completeness
-imports "../Main"
+imports Main
begin
subsection {* Preliminaries *}
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Jul 24 14:04:55 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Jul 24 14:08:29 2014 +0200
@@ -6,7 +6,7 @@
header {* Examples for the 'quickcheck' command *}
theory Quickcheck_Examples
-imports "../Complex_Main" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
+imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
begin
text {*