src/HOL/BNF_Wellorder_Constructions.thy
changeset 67091 1393c2340eec
parent 63561 fba08009ff3e
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4    where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
     1.5          "embed r r' f" and "embed r' r'' f'"
     1.6    using * ** unfolding ordLeq_def by blast
     1.7 -  hence "embed r r'' (f' o f)"
     1.8 +  hence "embed r r'' (f' \<circ> f)"
     1.9    using comp_embed[of r r' f r'' f'] by auto
    1.10    thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
    1.11  qed
    1.12 @@ -389,7 +389,7 @@
    1.13    where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
    1.14          "iso r r' f" and 3: "iso r' r'' f'"
    1.15    using * ** unfolding ordIso_def by auto
    1.16 -  hence "iso r r'' (f' o f)"
    1.17 +  hence "iso r r'' (f' \<circ> f)"
    1.18    using comp_iso[of r r' f r'' f'] by auto
    1.19    thus "r =o r''" unfolding ordIso_def using 1 by auto
    1.20  qed
    1.21 @@ -691,10 +691,10 @@
    1.22    ultimately
    1.23    have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
    1.24    moreover
    1.25 -  {have "embed r1 r3 (f23 o f12)"
    1.26 +  {have "embed r1 r3 (f23 \<circ> f12)"
    1.27     using 1 EMB23 0 by (auto simp add: comp_embed)
    1.28     hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
    1.29 -   using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto
    1.30 +   using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto
    1.31     hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
    1.32    }
    1.33    ultimately