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
Mon, 11 Apr 2016 15:26:58 +0200
changeset 62954 c5d0fdc260fa
parent 62953 48d935524988
child 62955 2fd4378caca2
tuned imports;
src/HOL/Library/Quotient_List.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Option.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Product.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Set.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Sum.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Quotient_List.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the list type\<close>
 
 theory Quotient_List
-imports Main Quotient_Set Quotient_Product Quotient_Option
+imports Quotient_Set Quotient_Product Quotient_Option
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Option.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the option type\<close>
 
 theory Quotient_Option
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Product.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the product type\<close>
 
 theory Quotient_Product
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Set.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the set type\<close>
 
 theory Quotient_Set
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Sum.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the sum type\<close>
 
 theory Quotient_Sum
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
isabelle