simplified use of tacticals;
authorwenzelm
Tue Feb 14 20:09:35 2012 +0100 (2012-02-14)
changeset 464684db76d47b51a
parent 46467 39e412f9ffdf
child 46469 0632b8e56e46
simplified use of tacticals;
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     1.1 --- a/src/HOL/Quotient.thy	Tue Feb 14 20:08:59 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Tue Feb 14 20:09:35 2012 +0100
     1.3 @@ -738,41 +738,41 @@
     1.4  
     1.5  method_setup lifting =
     1.6    {* Attrib.thms >> (fn thms => fn ctxt => 
     1.7 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
     1.8 +       SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *}
     1.9    {* lift theorems to quotient types *}
    1.10  
    1.11  method_setup lifting_setup =
    1.12    {* Attrib.thm >> (fn thm => fn ctxt => 
    1.13 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
    1.14 +       SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *}
    1.15    {* set up the three goals for the quotient lifting procedure *}
    1.16  
    1.17  method_setup descending =
    1.18 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
    1.19 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *}
    1.20    {* decend theorems to the raw level *}
    1.21  
    1.22  method_setup descending_setup =
    1.23 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
    1.24 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *}
    1.25    {* set up the three goals for the decending theorems *}
    1.26  
    1.27  method_setup partiality_descending =
    1.28 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
    1.29 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *}
    1.30    {* decend theorems to the raw level *}
    1.31  
    1.32  method_setup partiality_descending_setup =
    1.33    {* Scan.succeed (fn ctxt => 
    1.34 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
    1.35 +       SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *}
    1.36    {* set up the three goals for the decending theorems *}
    1.37  
    1.38  method_setup regularize =
    1.39 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
    1.40 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *}
    1.41    {* prove the regularization goals from the quotient lifting procedure *}
    1.42  
    1.43  method_setup injection =
    1.44 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
    1.45 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *}
    1.46    {* prove the rep/abs injection goals from the quotient lifting procedure *}
    1.47  
    1.48  method_setup cleaning =
    1.49 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
    1.50 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *}
    1.51    {* prove the cleaning goals from the quotient lifting procedure *}
    1.52  
    1.53  attribute_setup quot_lifted =
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Feb 14 20:08:59 2012 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Feb 14 20:09:35 2012 +0100
     2.3 @@ -364,7 +364,7 @@
     2.4    | (_ $
     2.5        (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     2.6        (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
     2.7 -        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
     2.8 +        => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
     2.9  
    2.10    | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
    2.11       (rtac @{thm refl} ORELSE'