equal
deleted
inserted
replaced
148 by (simp add: Quot_True_def) |
148 by (simp add: Quot_True_def) |
149 |
149 |
150 text {* Tactics for proving the lifted theorems *} |
150 text {* Tactics for proving the lifted theorems *} |
151 use "quotient_tacs.ML" |
151 use "quotient_tacs.ML" |
152 |
152 |
153 |
|
154 section {* Methods / Interface *} |
153 section {* Methods / Interface *} |
155 |
154 |
156 ML {* |
155 ML {* |
157 fun mk_method1 tac thms ctxt = |
156 fun mk_method1 tac thms ctxt = |
158 SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) |
157 SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) |
179 |
178 |
180 method_setup cleaning = |
179 method_setup cleaning = |
181 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
180 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
182 {* Proves automatically the cleaning goals from the lifting procedure. *} |
181 {* Proves automatically the cleaning goals from the lifting procedure. *} |
183 |
182 |
|
183 attribute_setup quot_lifted = |
|
184 {* Scan.succeed Quotient_Tacs.lifted_attr *} |
|
185 {* Lifting of theorems to quotient types. *} |
|
186 |
184 end |
187 end |
185 |
188 |