--- 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