# HG changeset patch
# User haftmann
# Date 1201269235 -3600
# Node ID 13b6c0b310056d644b892e886242bb501849247f
# Parent  ec39d7e40554a06126949adccd3f06e3c6483abb
clarified setup of method "normalization"

diff -r ec39d7e40554 -r 13b6c0b31005 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Fri Jan 25 14:53:52 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Fri Jan 25 14:53:55 2008 +0100
@@ -86,7 +86,7 @@
 
 text {* type bool *}
 
-lemmas [code func, code unfold] = imp_conv_disj
+lemmas [code func, code unfold, code post] = imp_conv_disj
 
 code_type bool
   (SML "bool")
@@ -147,8 +147,8 @@
 
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (fn k => CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) k
-    THEN TRYALL (resolve_tac [TrueI])
+    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
+    THEN' (fn k => TRY (rtac TrueI k))
   ))
 *} "solve goal by normalization"