changeset 62954 | c5d0fdc260fa |
parent 60500 | 903bb1495239 |
child 67399 | eab6ce8368fa |
62953:48d935524988 | 62954:c5d0fdc260fa |
---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>Quotient infrastructure for the sum type\<close> |
5 section \<open>Quotient infrastructure for the sum type\<close> |
6 |
6 |
7 theory Quotient_Sum |
7 theory Quotient_Sum |
8 imports Main Quotient_Syntax |
8 imports Quotient_Syntax |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Rules for the Quotient package\<close> |
11 subsection \<open>Rules for the Quotient package\<close> |
12 |
12 |
13 lemma rel_sum_map1: |
13 lemma rel_sum_map1: |