equal
deleted
inserted
replaced
179 method_setup cleaning = |
179 method_setup cleaning = |
180 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
180 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
181 {* Proves automatically the cleaning goals from the lifting procedure. *} |
181 {* Proves automatically the cleaning goals from the lifting procedure. *} |
182 |
182 |
183 attribute_setup quot_lifted = |
183 attribute_setup quot_lifted = |
184 {* Scan.succeed Quotient_Tacs.lifted_attr *} |
184 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
185 {* Lifting of theorems to quotient types. *} |
185 {* Lifting of theorems to quotient types. *} |
186 |
186 |
187 end |
187 end |
188 |
188 |