clarified setup of method "normalization"
authorhaftmann
Fri Jan 25 14:53:55 2008 +0100 (2008-01-25)
changeset 2596213b6c0b31005
parent 25961 ec39d7e40554
child 25963 07e08dad8a77
clarified setup of method "normalization"
src/HOL/Code_Setup.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Fri Jan 25 14:53:52 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Fri Jan 25 14:53:55 2008 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  text {* type bool *}
     1.6  
     1.7 -lemmas [code func, code unfold] = imp_conv_disj
     1.8 +lemmas [code func, code unfold, code post] = imp_conv_disj
     1.9  
    1.10  code_type bool
    1.11    (SML "bool")
    1.12 @@ -147,8 +147,8 @@
    1.13  
    1.14  method_setup normalization = {*
    1.15    Method.no_args (Method.SIMPLE_METHOD'
    1.16 -    (fn k => CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) k
    1.17 -    THEN TRYALL (resolve_tac [TrueI])
    1.18 +    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
    1.19 +    THEN' (fn k => TRY (rtac TrueI k))
    1.20    ))
    1.21  *} "solve goal by normalization"
    1.22