# HG changeset patch
# User wenzelm
# Date 1419173959 -3600
# Node ID 4e43651235b20b641824a574fe514b8f99cf2176
# Parent  115965966e15c9acc3c5e594207562c9e95e629c
recovered metis proof after 115965966e15 (Odd clash of type variables!?);

diff -r 115965966e15 -r 4e43651235b2 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 21 15:03:45 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 21 15:59:19 2014 +0100
@@ -1550,9 +1550,11 @@
 lemma Pfunc_mono[simp]:
 assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
 shows "Pfunc A B1 \<subseteq> Pfunc A B2"
-using assms in_mono unfolding Pfunc_def apply safe
-apply(case_tac "x a", auto)
-by (metis in_mono option.simps(5))
+using assms unfolding Pfunc_def
+apply safe
+apply (case_tac "x a", auto)
+apply (metis in_mono option.simps(5))
+done
 
 lemma card_of_Func_UNIV_UNIV:
 "|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"