equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close> |
8 section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close> |
9 |
9 |
10 theory Abstraction |
10 theory Abstraction |
11 imports "HOL-Library.FuncSet" |
11 imports HOL.FuncSet |
12 begin |
12 begin |
13 |
13 |
14 (* For Christoph Benzmüller *) |
14 (* For Christoph Benzmüller *) |
15 lemma "x < 1 \<and> ((=) = (=)) \<Longrightarrow> ((=) = (=)) \<and> x < (2::nat)" |
15 lemma "x < 1 \<and> ((=) = (=)) \<Longrightarrow> ((=) = (=)) \<and> x < (2::nat)" |
16 by (metis nat_1_add_1 trans_less_add2) |
16 by (metis nat_1_add_1 trans_less_add2) |