author  noschinl 
Wed, 18 Mar 2015 13:51:33 +0100  
changeset 59739  4ed50ebf5d36 
child 59975  da10875adf8e 
permissions  rwrr 
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 