59975

1 
(* Title: HOL/Library/Rewrite.thy


2 
Author: Christoph Traut, Lars Noschinski, TU Muenchen


3 


4 
Proof method "rewrite" with support for subtermselection 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
