src/HOL/Quotient.thy
changeset 45782 f82020ca3248
parent 45680 a61510361b89
child 45802 b16f976db515
     1.1 --- a/src/HOL/Quotient.thy	Mon Dec 05 15:10:15 2011 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Wed Dec 07 14:00:02 2011 +0000
     1.3 @@ -747,6 +747,15 @@
     1.4    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
     1.5    {* set up the three goals for the decending theorems *}
     1.6  
     1.7 +method_setup partiality_descending =
     1.8 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
     1.9 +  {* decend theorems to the raw level *}
    1.10 +
    1.11 +method_setup partiality_descending_setup =
    1.12 +  {* Scan.succeed (fn ctxt => 
    1.13 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
    1.14 +  {* set up the three goals for the decending theorems *}
    1.15 +
    1.16  method_setup regularize =
    1.17    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
    1.18    {* prove the regularization goals from the quotient lifting procedure *}