| changeset 41413 | 64cd30d6b0b8 |
| parent 39246 | 9e58f0499f57 |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/ex/ReflectionEx.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Wed Dec 29 17:34:41 2010 +0100 @@ -5,7 +5,7 @@ header {* Examples for generic reflection and reification *} theory ReflectionEx -imports Reflection +imports "~~/src/HOL/Library/Reflection" begin text{* This theory presents two methods: reify and reflection *}