equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Notions about functions *} |
6 header {* Notions about functions *} |
7 |
7 |
8 theory Fun |
8 theory Fun |
9 imports Set |
9 imports Complete_Lattice |
10 begin |
10 begin |
11 |
11 |
12 text{*As a simplification rule, it replaces all function equalities by |
12 text{*As a simplification rule, it replaces all function equalities by |
13 first-order equalities.*} |
13 first-order equalities.*} |
14 lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)" |
14 lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)" |