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