src/HOL/Library/Rewrite.thy
author noschinl
Mon, 13 Apr 2015 10:21:35 +0200
changeset 60047 58e5b16cbd94
parent 59975 da10875adf8e
child 60054 ef4878146485
permissions -rw-r--r--
enable \<hole> syntax for rewrite

(*  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::{}"
notation rewrite_HOLE ("HOLE")
notation rewrite_HOLE ("\<hole>")

lemma eta_expand:
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
  shows "f \<equiv> \<lambda>x. f x" .

ML_file "cconv.ML"
ML_file "rewrite.ML"

end