diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/HOL/Library/Reflection.thy Sun May 15 17:45:53 2011 +0200 @@ -41,6 +41,6 @@ val raw_eqs = eqs@ceqs in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end) end -*} "reflection" +*} end