author haftmann Fri, 24 Feb 2012 22:46:16 +0100 changeset 46663 7fe029e818c2 parent 46662 4e258158be38 child 46664 1f6c140f9c72
explicit is better than implicit
```--- 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 =)"```
```--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 18:46:01 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 22:46:16 2012 +0100
@@ -125,7 +125,7 @@
proof (intro conjI allI)
fix a r s
show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
-    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map.id)
+    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id)
have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
by (rule list_all2_refl'[OF e])
have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
@@ -500,7 +500,7 @@
and     r: "Quotient R2 Abs2 Rep2"
shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) op @ =
(Rep2 ---> Rep2 ---> Abs2) op @"
-  by (simp add: fun_eq_iff abs_o_rep[OF q] map.id)
+  by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)

lemma list_all2_app_l:
assumes a: "reflp R"```