Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned imports;
authorwenzelm
Thu, 24 Jul 2014 14:08:29 +0200
changeset 57645 ee55e667dedc
parent 57644 6ca1646b6f14
child 57646 da26d2d6346c
tuned imports;
src/HOL/Library/Quickcheck_Types.thy file | annotate | diff | comparison | revisions
src/HOL/Quickcheck_Examples/Completeness.thy file | annotate | diff | comparison | revisions
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy file | annotate | diff | comparison | revisions 
--- 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 {*
isabelle