equal
deleted
inserted
replaced
64 |
64 |
65 @{thm[display] o_inv_distrib[no_vars]} |
65 @{thm[display] o_inv_distrib[no_vars]} |
66 \rulename{o_inv_distrib} |
66 \rulename{o_inv_distrib} |
67 *} |
67 *} |
68 |
68 |
69 |
|
70 |
|
71 text{* |
69 text{* |
72 small sample proof |
70 small sample proof |
73 |
71 |
74 @{thm[display] ext[no_vars]} |
72 @{thm[display] ext[no_vars]} |
75 \rulename{ext} |
73 \rulename{ext} |
76 |
74 |
77 @{thm[display] expand_fun_eq[no_vars]} |
75 @{thm[display] fun_eq_iff[no_vars]} |
78 \rulename{expand_fun_eq} |
76 \rulename{fun_eq_iff} |
79 *} |
77 *} |
80 |
78 |
81 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
79 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
82 apply (simp add: expand_fun_eq inj_on_def) |
80 apply (simp add: fun_eq_iff inj_on_def) |
83 apply (auto) |
81 apply (auto) |
84 done |
82 done |
85 |
83 |
86 text{* |
84 text{* |
87 \begin{isabelle} |
85 \begin{isabelle} |