| changeset 45802 | b16f976db515 |
| parent 40820 | fd9c98ead9a9 |
| child 45806 | 0f1c049c147e |
--- a/src/HOL/Library/Quotient_List.thy Fri Dec 09 16:08:32 2011 +0100 +++ b/src/HOL/Library/Quotient_List.thy Fri Dec 09 18:07:04 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"