59975
|
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 |
|
59739
|
7 |
theory Rewrite
|
|
8 |
imports Main
|
|
9 |
begin
|
|
10 |
|
59975
|
11 |
consts rewrite_HOLE :: "'a::{}"
|
59739
|
12 |
notation rewrite_HOLE ("HOLE")
|
|
13 |
notation rewrite_HOLE ("\<box>")
|
|
14 |
|
|
15 |
lemma eta_expand:
|
59975
|
16 |
fixes f :: "'a::{} \<Rightarrow> 'b::{}"
|
|
17 |
shows "f \<equiv> \<lambda>x. f x" .
|
59739
|
18 |
|
|
19 |
ML_file "cconv.ML"
|
|
20 |
ML_file "rewrite.ML"
|
|
21 |
|
|
22 |
end
|