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
wenzelm@59975
     1
(*  Title:      HOL/Library/Rewrite.thy
wenzelm@59975
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
wenzelm@59975
     3
wenzelm@59975
     4
Proof method "rewrite" with support for subterm-selection based on patterns.
wenzelm@59975
     5
*)
wenzelm@59975
     6
noschinl@59739
     7
theory Rewrite
noschinl@59739
     8
imports Main
noschinl@59739
     9
begin
noschinl@59739
    10
wenzelm@59975
    11
consts rewrite_HOLE :: "'a::{}"
noschinl@59739
    12
notation rewrite_HOLE ("HOLE")
noschinl@60047
    13
notation rewrite_HOLE ("\<hole>")
noschinl@59739
    14
noschinl@59739
    15
lemma eta_expand:
wenzelm@59975
    16
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
wenzelm@59975
    17
  shows "f \<equiv> \<lambda>x. f x" .
noschinl@59739
    18
noschinl@59739
    19
ML_file "cconv.ML"
noschinl@59739
    20
ML_file "rewrite.ML"
noschinl@59739
    21
noschinl@59739
    22
end