| changeset 22199 | b617ddd200eb |
| parent 21879 | a3efbae45735 |
| child 23546 | c8a1bd9585a0 |
--- a/src/HOL/ex/Reflection.thy Fri Jan 26 13:59:06 2007 +0100 +++ b/src/HOL/ex/Reflection.thy Sun Jan 28 11:52:52 2007 +0100 @@ -7,11 +7,12 @@ theory Reflection imports Main -uses ("reflection.ML") + uses ("reflection.ML") begin lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" by (blast intro: ext) + use "reflection.ML" method_setup reify = {*