| author | noschinl |
| Wed, 18 Mar 2015 13:51:33 +0100 | |
| changeset 59739 | 4ed50ebf5d36 |
| child 59975 | da10875adf8e |
| permissions | -rw-r--r-- |
| 59739 | 1 |
theory Rewrite |
2 |
imports Main |
|
3 |
begin |
|
4 |
||
5 |
consts rewrite_HOLE :: "'a :: {}"
|
|
6 |
notation rewrite_HOLE ("HOLE")
|
|
7 |
notation rewrite_HOLE ("\<box>")
|
|
8 |
||
9 |
lemma eta_expand: |
|
10 |
fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
|
|
11 |
by (rule reflexive) |
|
12 |
||
13 |
ML_file "cconv.ML" |
|
14 |
ML_file "rewrite.ML" |
|
15 |
setup Rewrite.setup |
|
16 |
||
17 |
end |