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_equivps} 1) (ith 1)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 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(unfold perm_kind_def perm_ty_def perm_trm_def) |
|
274 apply(tactic {* clean_tac @{context} 1 *}) |
273 done |
275 done |
274 |
276 |
275 (* Does not work: |
277 (* Does not work: |
276 lemma |
278 lemma |
277 assumes a0: "P1 TYP" |
279 assumes a0: "P1 TYP" |