| changeset 48029 | 9d9c9069abbc |
| parent 48028 | a5377f6d9f14 |
| child 48034 | 1c5171abe5cc |
--- a/src/HOL/ex/FinFunPred.thy Tue May 29 15:31:58 2012 +0200 +++ b/src/HOL/ex/FinFunPred.thy Tue May 29 16:08:12 2012 +0200 @@ -195,7 +195,7 @@ lemma iso_finfun_eq [code_unfold]: "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B" -by(simp add: expand_finfun_eq) +by(simp only: expand_finfun_eq) lemma iso_finfun_sup [code_unfold]: "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"