src/HOL/Quotient.thy
changeset 37564 a47bb386b238
parent 37493 2377d246a631
child 37593 2505feaf2d70
     1.1 --- a/src/HOL/Quotient.thy	Mon Jun 28 07:38:39 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Mon Jun 28 09:48:36 2010 +0200
     1.3 @@ -768,7 +768,7 @@
     1.4    {* lifts theorems to quotient types *}
     1.5  
     1.6  method_setup lifting_setup =
     1.7 -  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
     1.8 +  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
     1.9    {* sets up the three goals for the quotient lifting procedure *}
    1.10  
    1.11  method_setup regularize =