diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Fri Mar 23 14:18:43 2012 +0100 +++ b/src/HOL/Library/Quotient_List.thy Fri Mar 23 14:20:09 2012 +0100 @@ -8,8 +8,6 @@ imports Main Quotient_Syntax begin -declare [[map list = list_all2]] - lemma map_id [id_simps]: "map id = id" by (fact List.map.id) @@ -75,6 +73,8 @@ by (induct xs ys rule: list_induct2') auto qed +declare [[map list = (list_all2, list_quotient)]] + lemma cons_prs [quot_preserve]: assumes q: "Quotient R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"