309 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
319 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
310 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
320 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
311 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
321 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
312 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
322 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
313 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
323 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
|
324 ML_prf {* |
|
325 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
|
326 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
|
327 *} |
|
328 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
329 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
330 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
331 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
332 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
333 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
334 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
335 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
336 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
337 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
338 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
339 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
340 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
341 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
342 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
343 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
344 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
345 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
346 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
347 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
348 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
349 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
350 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
351 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
352 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
353 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
354 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
|
355 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
356 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
357 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
358 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*}) |
|
359 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
360 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
361 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
362 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
363 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
364 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
365 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
366 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
367 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
368 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
369 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
370 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
371 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
372 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
373 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
374 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
375 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
376 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
377 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
378 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
379 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
380 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
381 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
382 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
383 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
384 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
385 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
386 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
387 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
388 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*}) |
|
389 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
390 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
391 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
392 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*}) |
|
393 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
394 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
395 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
396 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*}) |
|
397 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms KPi_rsp}) 1*}) |
|
398 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
399 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
400 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
|
401 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
402 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
403 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
404 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
405 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
406 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
|
407 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
408 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
409 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
410 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
411 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
412 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
413 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
414 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
415 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
416 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
417 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
418 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
419 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
420 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
421 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
422 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*}) |
|
423 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
424 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
425 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
426 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*}) |
|
427 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
428 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
429 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
430 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_rsp}) 1*}) |
|
431 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
432 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
433 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
434 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_rsp}) 1*}) |
|
435 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
436 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
437 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
|
438 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*}) |
|
439 |
|
440 |
|
441 |
|
442 |
314 |
443 |
315 |
444 |
316 |
445 |
317 |
446 |
318 |
447 |