src/HOL/Library/Rewrite.thy
author noschinl
Mon Apr 13 10:21:35 2015 +0200 (2015-04-13)
changeset 60047 58e5b16cbd94
parent 59975 da10875adf8e
child 60054 ef4878146485
permissions -rw-r--r--
enable \<hole> syntax for rewrite
     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 
     7 theory Rewrite
     8 imports Main
     9 begin
    10 
    11 consts rewrite_HOLE :: "'a::{}"
    12 notation rewrite_HOLE ("HOLE")
    13 notation rewrite_HOLE ("\<hole>")
    14 
    15 lemma eta_expand:
    16   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    17   shows "f \<equiv> \<lambda>x. f x" .
    18 
    19 ML_file "cconv.ML"
    20 ML_file "rewrite.ML"
    21 
    22 end