| changeset 45806 | 0f1c049c147e |
| parent 45803 | fe44c0b216ef |
| parent 45802 | b16f976db515 |
| child 46663 | 7fe029e818c2 |
--- a/src/HOL/Library/Quotient_List.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Library/Quotient_List.thy Sat Dec 10 13:00:58 2011 +0100 @@ -8,7 +8,7 @@ imports Main Quotient_Syntax begin -declare [[map list = (map, list_all2)]] +declare [[map list = list_all2]] lemma map_id [id_simps]: "map id = id"