src/HOL/List.ML
changeset 10832 e33b47e4246d
parent 10709 7a29b71d6352
child 11265 4f2e6c87a57f
     1.1 --- a/src/HOL/List.ML	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -448,7 +448,7 @@
     1.4  qed "set_rev";
     1.5  Addsimps [set_rev];
     1.6  
     1.7 -Goal "set(map f xs) = f``(set xs)";
     1.8 +Goal "set(map f xs) = f`(set xs)";
     1.9  by (induct_tac "xs" 1);
    1.10  by Auto_tac;
    1.11  qed "set_map";
    1.12 @@ -574,7 +574,7 @@
    1.13  qed "Nil_eq_concat_conv";
    1.14  AddIffs [Nil_eq_concat_conv];
    1.15  
    1.16 -Goal  "set(concat xs) = Union(set `` set xs)";
    1.17 +Goal  "set(concat xs) = Union(set ` set xs)";
    1.18  by (induct_tac "xs" 1);
    1.19  by Auto_tac;
    1.20  qed"set_concat";