src/HOL/Quotient.thy
changeset 37593 2505feaf2d70
parent 37564 a47bb386b238
child 37986 3b3187adf292
     1.1 --- a/src/HOL/Quotient.thy	Mon Jun 28 16:20:39 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Tue Jun 29 01:38:29 2010 +0100
     1.3 @@ -764,13 +764,23 @@
     1.4  subsection {* Methods / Interface *}
     1.5  
     1.6  method_setup lifting =
     1.7 -  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
     1.8 +  {* Attrib.thms >> (fn thms => fn ctxt => 
     1.9 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
    1.10    {* lifts theorems to quotient types *}
    1.11  
    1.12  method_setup lifting_setup =
    1.13 -  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
    1.14 +  {* Attrib.thm >> (fn thm => fn ctxt => 
    1.15 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
    1.16    {* sets up the three goals for the quotient lifting procedure *}
    1.17  
    1.18 +method_setup descending =
    1.19 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
    1.20 +  {* decends 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 +  {* sets up the three goals for the decending theorems *}
    1.25 +
    1.26  method_setup regularize =
    1.27    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
    1.28    {* proves the regularization goals from the quotient lifting procedure *}