explicit is better than implicit
authorhaftmann
Fri Feb 24 22:46:16 2012 +0100 (2012-02-24)
changeset 466637fe029e818c2
parent 46662 4e258158be38
child 46664 1f6c140f9c72
explicit is better than implicit
src/HOL/Library/Quotient_List.thy
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Feb 24 18:46:01 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Feb 24 22:46:16 2012 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  lemma map_id [id_simps]:
     1.6    "map id = id"
     1.7 -  by (fact map.id)
     1.8 +  by (fact List.map.id)
     1.9  
    1.10  lemma list_all2_eq [id_simps]:
    1.11    "list_all2 (op =) = (op =)"
     2.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 18:46:01 2012 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 22:46:16 2012 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  proof (intro conjI allI)
     2.5    fix a r s
     2.6    show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
     2.7 -    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map.id)
     2.8 +    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id)
     2.9    have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    2.10      by (rule list_all2_refl'[OF e])
    2.11    have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    2.12 @@ -500,7 +500,7 @@
    2.13    and     r: "Quotient R2 Abs2 Rep2"
    2.14    shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) op @ =
    2.15      (Rep2 ---> Rep2 ---> Abs2) op @"
    2.16 -  by (simp add: fun_eq_iff abs_o_rep[OF q] map.id)
    2.17 +  by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)
    2.18  
    2.19  lemma list_all2_app_l:
    2.20    assumes a: "reflp R"