summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Rewrite.thy

changeset 59975 | da10875adf8e |

parent 59739 | 4ed50ebf5d36 |

child 60047 | 58e5b16cbd94 |

--- a/src/HOL/Library/Rewrite.thy Wed Apr 08 21:08:26 2015 +0200 +++ b/src/HOL/Library/Rewrite.thy Wed Apr 08 21:24:27 2015 +0200 @@ -1,17 +1,22 @@ +(* 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 :: {}" +consts rewrite_HOLE :: "'a::{}" notation rewrite_HOLE ("HOLE") notation rewrite_HOLE ("\<box>") lemma eta_expand: - fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)" - by (rule reflexive) + fixes f :: "'a::{} \<Rightarrow> 'b::{}" + shows "f \<equiv> \<lambda>x. f x" . ML_file "cconv.ML" ML_file "rewrite.ML" -setup Rewrite.setup end