equal
deleted
inserted
replaced
77 @{thm[display] expand_fun_eq[no_vars]} |
77 @{thm[display] expand_fun_eq[no_vars]} |
78 \rulename{expand_fun_eq} |
78 \rulename{expand_fun_eq} |
79 *} |
79 *} |
80 |
80 |
81 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
81 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
82 apply (simp add: expand_fun_eq inj_on_def o_def) |
82 apply (simp add: expand_fun_eq inj_on_def) |
83 apply (auto) |
83 apply (auto) |
84 done |
84 done |
85 |
85 |
86 text{* |
86 text{* |
87 \begin{isabelle} |
87 \begin{isabelle} |