src/HOL/HOL.thy
changeset 41184 5c6f44d22f51
parent 41042 8275f52ac991
child 41229 d797baa3d57c
child 41247 c5cb19ecbd41
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 15 09:47:12 2010 +0100
     1.3 @@ -1976,7 +1976,7 @@
     1.4  
     1.5  method_setup normalization = {*
     1.6    Scan.succeed (K (SIMPLE_METHOD'
     1.7 -    (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))))
     1.8 +    (CHANGED_PROP o (CONVERSION Nbe.dynamic_conv THEN' (fn k => TRY (rtac TrueI k))))))
     1.9  *} "solve goal by normalization"
    1.10  
    1.11