--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Rewrite.thy	Wed Mar 18 13:51:33 2015 +0100
@@ -0,0 +1,17 @@
+theory Rewrite
+imports Main
+begin
+
+consts rewrite_HOLE :: "'a :: {}"
+notation rewrite_HOLE ("HOLE")
+notation rewrite_HOLE ("\<box>")
+
+lemma eta_expand:
+  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
+  by (rule reflexive)
+
+ML_file "cconv.ML"
+ML_file "rewrite.ML"
+setup Rewrite.setup
+
+end