| changeset 45806 | 0f1c049c147e |
| parent 45803 | fe44c0b216ef |
| parent 45802 | b16f976db515 |
| child 46663 | 7fe029e818c2 |
| 45805:3c609e8785f2 | 45806:0f1c049c147e |
|---|---|
6 |
6 |
7 theory Quotient_List |
7 theory Quotient_List |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
10 |
10 |
11 declare [[map list = (map, list_all2)]] |
11 declare [[map list = list_all2]] |
12 |
12 |
13 lemma map_id [id_simps]: |
13 lemma map_id [id_simps]: |
14 "map id = id" |
14 "map id = id" |
15 by (fact map.id) |
15 by (fact map.id) |
16 |
16 |