changeset 52182 | 57b4fdc59d3b |
parent 49310 | 6e30078de4f0 |
child 54435 | 4a655e62ad34 |
--- a/src/HOL/Cardinals/Wellfounded_More_Base.thy Fri May 24 17:37:06 2013 +0200 +++ b/src/HOL/Cardinals/Wellfounded_More_Base.thy Fri May 24 18:11:57 2013 +0200 @@ -158,7 +158,7 @@ ultimately show ?thesis by blast next assume Case2: "\<not> r \<le> Id" - hence 1: "Field r = Field(r - Id)" using rel.Total_Id_Field LI + hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI unfolding order_on_defs by blast show ?thesis proof