equal
deleted
inserted
replaced
149 |
149 |
150 |
150 |
151 section {* Methods / Interface *} |
151 section {* Methods / Interface *} |
152 |
152 |
153 ML {* |
153 ML {* |
154 fun mk_method1 tac thm ctxt = |
154 fun mk_method1 tac thms ctxt = |
155 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
155 SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) |
156 |
156 |
157 fun mk_method2 tac ctxt = |
157 fun mk_method2 tac ctxt = |
158 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
158 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
159 *} |
159 *} |
160 |
160 |
161 method_setup lifting = |
161 method_setup lifting = |
162 {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *} |
162 {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} |
163 {* Lifting of theorems to quotient types. *} |
163 {* Lifting of theorems to quotient types. *} |
164 |
164 |
165 method_setup lifting_setup = |
165 method_setup lifting_setup = |
166 {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} |
166 {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} |
167 {* Sets up the three goals for the lifting procedure. *} |
167 {* Sets up the three goals for the lifting procedure. *} |