src/HOL/Library/Rewrite.thy
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60047 58e5b16cbd94
--- a/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:08:26 2015 +0200
+++ b/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:24:27 2015 +0200
@@ -1,17 +1,22 @@
+(*  Title:      HOL/Library/Rewrite.thy
+    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
+
+Proof method "rewrite" with support for subterm-selection based on patterns.
+*)
+
 theory Rewrite
 imports Main
 begin
 
-consts rewrite_HOLE :: "'a :: {}"
+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)
+  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
+  shows "f \<equiv> \<lambda>x. f x" .
 
 ML_file "cconv.ML"
 ML_file "rewrite.ML"
-setup Rewrite.setup
 
 end