src/HOL/Quotient.thy
changeset 37593 2505feaf2d70
parent 37564 a47bb386b238
child 37986 3b3187adf292
--- a/src/HOL/Quotient.thy	Mon Jun 28 16:20:39 2010 +0100
+++ b/src/HOL/Quotient.thy	Tue Jun 29 01:38:29 2010 +0100
@@ -764,13 +764,23 @@
 subsection {* Methods / Interface *}
 
 method_setup lifting =
-  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => 
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
-  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+  {* Attrib.thm >> (fn thm => fn ctxt => 
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
+method_setup descending =
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
+  {* decends theorems to the raw level *}
+
+method_setup descending_setup =
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
+  {* sets up the three goals for the decending theorems *}
+
 method_setup regularize =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   {* proves the regularization goals from the quotient lifting procedure *}