equal
deleted
inserted
replaced
|
1 (* Title: HOL/Library/Rewrite.thy |
|
2 Author: Christoph Traut, Lars Noschinski, TU Muenchen |
|
3 |
|
4 Proof method "rewrite" with support for subterm-selection based on patterns. |
|
5 *) |
|
6 |
1 theory Rewrite |
7 theory Rewrite |
2 imports Main |
8 imports Main |
3 begin |
9 begin |
4 |
10 |
5 consts rewrite_HOLE :: "'a :: {}" |
11 consts rewrite_HOLE :: "'a::{}" |
6 notation rewrite_HOLE ("HOLE") |
12 notation rewrite_HOLE ("HOLE") |
7 notation rewrite_HOLE ("\<box>") |
13 notation rewrite_HOLE ("\<box>") |
8 |
14 |
9 lemma eta_expand: |
15 lemma eta_expand: |
10 fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)" |
16 fixes f :: "'a::{} \<Rightarrow> 'b::{}" |
11 by (rule reflexive) |
17 shows "f \<equiv> \<lambda>x. f x" . |
12 |
18 |
13 ML_file "cconv.ML" |
19 ML_file "cconv.ML" |
14 ML_file "rewrite.ML" |
20 ML_file "rewrite.ML" |
15 setup Rewrite.setup |
|
16 |
21 |
17 end |
22 end |