equal
deleted
inserted
replaced
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
270 ML_prf {* PolyML.profiling 1 *} |
270 ML_prf {* PolyML.profiling 1 *} |
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
272 *) |
272 *) |
273 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
273 apply(tactic {* all_inj_repabs_tac' @{context} quot rel_refl trans2 1 *}) |
|
274 (*apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})*) |
274 done |
275 done |
275 |
276 |
276 (* Does not work: |
277 (* Does not work: |
277 lemma |
278 lemma |
278 assumes a0: "P1 TYP" |
279 assumes a0: "P1 TYP" |