src/HOL/Library/Rewrite.thy
author noschinl
Wed Mar 18 13:51:33 2015 +0100 (2015-03-18)
changeset 59739 4ed50ebf5d36
child 59975 da10875adf8e
permissions -rw-r--r--
added proof method rewrite
noschinl@59739
     1
theory Rewrite
noschinl@59739
     2
imports Main
noschinl@59739
     3
begin
noschinl@59739
     4
noschinl@59739
     5
consts rewrite_HOLE :: "'a :: {}"
noschinl@59739
     6
notation rewrite_HOLE ("HOLE")
noschinl@59739
     7
notation rewrite_HOLE ("\<box>")
noschinl@59739
     8
noschinl@59739
     9
lemma eta_expand:
noschinl@59739
    10
  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
noschinl@59739
    11
  by (rule reflexive)
noschinl@59739
    12
noschinl@59739
    13
ML_file "cconv.ML"
noschinl@59739
    14
ML_file "rewrite.ML"
noschinl@59739
    15
setup Rewrite.setup
noschinl@59739
    16
noschinl@59739
    17
end