src/HOL/Library/Rewrite.thy
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60047 58e5b16cbd94
equal deleted inserted replaced
59974:b911c8ba0b69 59975:da10875adf8e
       
     1 (*  Title:      HOL/Library/Rewrite.thy
       
     2     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
       
     3 
       
     4 Proof method "rewrite" with support for subterm-selection based on patterns.
       
     5 *)
       
     6 
     1 theory Rewrite
     7 theory Rewrite
     2 imports Main
     8 imports Main
     3 begin
     9 begin
     4 
    10 
     5 consts rewrite_HOLE :: "'a :: {}"
    11 consts rewrite_HOLE :: "'a::{}"
     6 notation rewrite_HOLE ("HOLE")
    12 notation rewrite_HOLE ("HOLE")
     7 notation rewrite_HOLE ("\<box>")
    13 notation rewrite_HOLE ("\<box>")
     8 
    14 
     9 lemma eta_expand:
    15 lemma eta_expand:
    10   fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
    16   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    11   by (rule reflexive)
    17   shows "f \<equiv> \<lambda>x. f x" .
    12 
    18 
    13 ML_file "cconv.ML"
    19 ML_file "cconv.ML"
    14 ML_file "rewrite.ML"
    20 ML_file "rewrite.ML"
    15 setup Rewrite.setup
       
    16 
    21 
    17 end
    22 end