src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 55604 42e4e8c2e8dc
parent 55059 ef2e0fb783c6
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 13:53:26 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 15:14:37 2014 +0100
     1.3 @@ -400,7 +400,8 @@
     1.4    proof (cases "Field p2 = {}")
     1.5      case True
     1.6      with n have "Field r2 = {}" .
     1.7 -    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
     1.8 +    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
     1.9 +      by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
    1.10      thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
    1.11    next
    1.12      case False with True have "|Field (p1 ^c p2)| =o czero"