src/HOL/Code_Setup.thy
changeset 25962 13b6c0b31005
parent 25916 d957d9982241
child 26975 103dca19ef2e
     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