changeset 46663 | 7fe029e818c2 |
parent 45806 | 0f1c049c147e |
child 47094 | 1a7ad2601cb5 |
--- a/src/HOL/Library/Quotient_List.thy Fri Feb 24 18:46:01 2012 +0100 +++ b/src/HOL/Library/Quotient_List.thy Fri Feb 24 22:46:16 2012 +0100 @@ -12,7 +12,7 @@ lemma map_id [id_simps]: "map id = id" - by (fact map.id) + by (fact List.map.id) lemma list_all2_eq [id_simps]: "list_all2 (op =) = (op =)"