equal
deleted
inserted
replaced
89 Application is made explicit for constants occurring with varying |
89 Application is made explicit for constants occurring with varying |
90 numbers of arguments. This is achieved by the introduction of the |
90 numbers of arguments. This is achieved by the introduction of the |
91 following constant. |
91 following constant. |
92 *} |
92 *} |
93 |
93 |
94 definition fun_app where "fun_app f x = f x" |
94 definition fun_app where "fun_app f = f" |
95 |
95 |
96 text {* |
96 text {* |
97 Some solvers support a theory of arrays which can be used to encode |
97 Some solvers support a theory of arrays which can be used to encode |
98 higher-order functions. The following set of lemmas specifies the |
98 higher-order functions. The following set of lemmas specifies the |
99 properties of such (extensional) arrays. |
99 properties of such (extensional) arrays. |