summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 11 Apr 2016 15:26:58 +0200 | |

changeset 62954 | c5d0fdc260fa |

parent 62953 | 48d935524988 |

child 62955 | 2fd4378caca2 |

tuned imports;

--- 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>