| changeset 63092 | a949b2a5f51d |
| parent 61799 | 4cf66f21b764 |
| child 67091 | 1393c2340eec |
--- a/src/HOL/BNF_Wellorder_Embedding.thy Fri May 13 20:22:02 2016 +0200 +++ b/src/HOL/BNF_Wellorder_Embedding.thy Fri May 13 20:24:10 2016 +0200 @@ -986,7 +986,7 @@ lemma iso_Field: "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'" -using assms by (auto simp add: iso_def bij_betw_def) +by (auto simp add: iso_def bij_betw_def) lemma iso_iff: assumes "Well_order r"