more conventional eval_tac vs. method_setup "eval";
authorwenzelm
Wed Jan 11 21:04:22 2012 +0100 (2012-01-11)
changeset 46190a42c5f23109f
parent 46189 7f6668317e24
child 46191 a88546428c2a
more conventional eval_tac vs. method_setup "eval";
clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Jan 11 18:02:59 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Jan 11 21:04:22 2012 +0100
     1.3 @@ -1906,19 +1906,20 @@
     1.4  subsubsection {* Evaluation and normalization by evaluation *}
     1.5  
     1.6  ML {*
     1.7 -fun gen_eval_method conv ctxt = SIMPLE_METHOD'
     1.8 -  (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)
     1.9 -    THEN' rtac TrueI)
    1.10 +fun eval_tac ctxt =
    1.11 +  let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
    1.12 +  in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    1.13  *}
    1.14  
    1.15 -method_setup eval = {*
    1.16 -  Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
    1.17 -*} "solve goal by evaluation"
    1.18 +method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
    1.19 +  "solve goal by evaluation"
    1.20  
    1.21  method_setup normalization = {*
    1.22 -  Scan.succeed (fn ctxt => SIMPLE_METHOD'
    1.23 -    (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
    1.24 -      THEN' (fn k => TRY (rtac TrueI k)))))
    1.25 +  Scan.succeed (fn ctxt =>
    1.26 +    SIMPLE_METHOD'
    1.27 +      (CHANGED_PROP o
    1.28 +        (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
    1.29 +          THEN_ALL_NEW (TRY o rtac TrueI))))
    1.30  *} "solve goal by normalization"
    1.31  
    1.32