| changeset 63092 | a949b2a5f51d |
| parent 62329 | 9f7fa08d2307 |
| child 63714 | b62f4f765353 |
--- a/src/HOL/BNF_Def.thy Fri May 13 20:22:02 2016 +0200 +++ b/src/HOL/BNF_Def.thy Fri May 13 20:24:10 2016 +0200 @@ -248,7 +248,7 @@ by (simp add: eq_onp_def) lemma eq_onp_same_args: "eq_onp P x x = P x" - using assms by (auto simp add: eq_onp_def) + by (auto simp add: eq_onp_def) lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x" unfolding eq_onp_def by blast