src/HOL/Library/Rewrite.thy
author wenzelm
Wed Apr 08 21:24:27 2015 +0200 (2015-04-08)
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60047 58e5b16cbd94
permissions -rw-r--r--
more standard Isabelle/ML tool setup;
proper file headers;
tuned whitespace;
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@59739
    13
notation rewrite_HOLE ("\<box>")
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