src/HOL/Library/Rewrite.thy
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60047 58e5b16cbd94
     1.1 --- a/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:08:26 2015 +0200
     1.2 +++ b/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:24:27 2015 +0200
     1.3 @@ -1,17 +1,22 @@
     1.4 +(*  Title:      HOL/Library/Rewrite.thy
     1.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     1.6 +
     1.7 +Proof method "rewrite" with support for subterm-selection based on patterns.
     1.8 +*)
     1.9 +
    1.10  theory Rewrite
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -consts rewrite_HOLE :: "'a :: {}"
    1.15 +consts rewrite_HOLE :: "'a::{}"
    1.16  notation rewrite_HOLE ("HOLE")
    1.17  notation rewrite_HOLE ("\<box>")
    1.18  
    1.19  lemma eta_expand:
    1.20 -  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
    1.21 -  by (rule reflexive)
    1.22 +  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    1.23 +  shows "f \<equiv> \<lambda>x. f x" .
    1.24  
    1.25  ML_file "cconv.ML"
    1.26  ML_file "rewrite.ML"
    1.27 -setup Rewrite.setup
    1.28  
    1.29  end