equal
deleted
inserted
replaced
263 in |
263 in |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 ML {* val cheat_equivp = Unsynchronized.ref true *} |
268 (* This one is not needed for the proper examples *) |
|
269 ML {* val cheat_equivp = Unsynchronized.ref false *} |
269 |
270 |
270 (* These 4 are not needed any more *) |
271 (* These 4 are not needed any more *) |
271 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
272 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
272 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
273 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
273 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
274 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |