less flex-flex pairs (thanks to Lars' statistics)
authortraytel
Thu Feb 20 13:53:26 2014 +0100 (2014-02-20)
changeset 5560348596c45bf7f
parent 55602 257bd115fcca
child 55604 42e4e8c2e8dc
less flex-flex pairs (thanks to Lars' statistics)
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Constructions_on_Wellorders.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 11:40:03 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 13:53:26 2014 +0100
     1.3 @@ -414,7 +414,7 @@
     1.4    let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
     1.5    have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
     1.6    using * unfolding inj_on_def by auto
     1.7 -  thus ?thesis using card_of_ordLeq by fast
     1.8 +  thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
     1.9  qed
    1.10  
    1.11  corollary Card_order_singl_ordLeq:
     2.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Feb 20 11:40:03 2014 +0100
     2.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Feb 20 13:53:26 2014 +0100
     2.3 @@ -1652,8 +1652,7 @@
     2.4        qed(insert h, unfold Func_def Func_map_def, auto)
     2.5      qed
     2.6      moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
     2.7 -    using inv_into_into j2A2 B1 A2 inv_into_into
     2.8 -    unfolding j1_def image_def by fast+
     2.9 +    using j2A2 B1 A2 unfolding j1_def image_def by (fast intro: inv_into_into)+
    2.10      ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
    2.11      unfolding Func_map_def[abs_def] unfolding image_def by auto
    2.12    qed(insert B1 Func_map[OF _ _ A2(2)], auto)