src/HOL/Quotient.thy
changeset 42814 5af15f1e2ef6
parent 42334 8e58cc1390c7
child 44204 3cdc4176638c
     1.1 --- a/src/HOL/Quotient.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -728,36 +728,36 @@
     1.4  method_setup lifting =
     1.5    {* Attrib.thms >> (fn thms => fn ctxt => 
     1.6         SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
     1.7 -  {* lifts theorems to quotient types *}
     1.8 +  {* lift theorems to quotient types *}
     1.9  
    1.10  method_setup lifting_setup =
    1.11    {* Attrib.thm >> (fn thm => fn ctxt => 
    1.12         SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
    1.13 -  {* sets up the three goals for the quotient lifting procedure *}
    1.14 +  {* set up the three goals for the quotient lifting procedure *}
    1.15  
    1.16  method_setup descending =
    1.17    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
    1.18 -  {* decends theorems to the raw level *}
    1.19 +  {* decend theorems to the raw level *}
    1.20  
    1.21  method_setup descending_setup =
    1.22    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
    1.23 -  {* sets up the three goals for the decending theorems *}
    1.24 +  {* set 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 *}
    1.29 +  {* prove the regularization goals from the quotient lifting procedure *}
    1.30  
    1.31  method_setup injection =
    1.32    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
    1.33 -  {* proves the rep/abs injection goals from the quotient lifting procedure *}
    1.34 +  {* prove the rep/abs injection goals from the quotient lifting procedure *}
    1.35  
    1.36  method_setup cleaning =
    1.37    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
    1.38 -  {* proves the cleaning goals from the quotient lifting procedure *}
    1.39 +  {* prove the cleaning goals from the quotient lifting procedure *}
    1.40  
    1.41  attribute_setup quot_lifted =
    1.42    {* Scan.succeed Quotient_Tacs.lifted_attrib *}
    1.43 -  {* lifts theorems to quotient types *}
    1.44 +  {* lift theorems to quotient types *}
    1.45  
    1.46  no_notation
    1.47    rel_conj (infixr "OOO" 75) and