author | haftmann |
Thu, 02 Sep 2010 09:13:16 +0200 | |
changeset 39015 | 81a70e2835b6 |
parent 38981 | 7cf8beb31e0f |
child 39016 | caad9d509bc4 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Thu Sep 02 08:40:25 2010 +0200 +++ b/src/HOL/HOL.thy Thu Sep 02 09:13:16 2010 +0200 @@ -1996,7 +1996,7 @@ method_setup normalization = {* Scan.succeed (K (SIMPLE_METHOD' - (CHANGED_PROP o CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))) + (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))) *} "solve goal by normalization"