src/HOL/Library/Quotient_List.thy
changeset 47094 1a7ad2601cb5
parent 46663 7fe029e818c2
child 47308 9caab698dbe4
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -declare [[map list = list_all2]]
     1.8 -
     1.9  lemma map_id [id_simps]:
    1.10    "map id = id"
    1.11    by (fact List.map.id)
    1.12 @@ -75,6 +73,8 @@
    1.13      by (induct xs ys rule: list_induct2') auto
    1.14  qed
    1.15  
    1.16 +declare [[map list = (list_all2, list_quotient)]]
    1.17 +
    1.18  lemma cons_prs [quot_preserve]:
    1.19    assumes q: "Quotient R Abs Rep"
    1.20    shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"