src/HOL/BNF_Wellorder_Constructions.thy
changeset 63092 a949b2a5f51d
parent 63040 eb4ddd18d635
child 63561 fba08009ff3e
     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:22:02 2016 +0200
     1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:24:10 2016 +0200
     1.3 @@ -570,7 +570,7 @@
     1.4  
     1.5  lemma not_ordLess_ordIso:
     1.6  "r <o r' \<Longrightarrow> \<not> r =o r'"
     1.7 -using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
     1.8 +using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
     1.9  
    1.10  lemma not_ordLeq_iff_ordLess:
    1.11  assumes WELL: "Well_order r" and WELL': "Well_order r'"
    1.12 @@ -584,7 +584,7 @@
    1.13  
    1.14  lemma ordLess_transitive[trans]:
    1.15  "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
    1.16 -using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
    1.17 +using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
    1.18  
    1.19  corollary ordLess_trans: "trans ordLess"
    1.20  unfolding trans_def using ordLess_transitive by blast
    1.21 @@ -1003,7 +1003,7 @@
    1.22  
    1.23  lemma Well_order_dir_image:
    1.24  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
    1.25 -using assms unfolding well_order_on_def
    1.26 +unfolding well_order_on_def
    1.27  using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
    1.28    dir_image_minus_Id[of f r]
    1.29    subset_inj_on[of f "Field r" "Field(r - Id)"]