267 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
281 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
268 ML_prf {* |
282 ML_prf {* |
269 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
283 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
270 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
284 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
271 *} |
285 *} |
272 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
286 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
273 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
287 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
274 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
288 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
275 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
289 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
276 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
290 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
277 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
291 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
278 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
292 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
279 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
293 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
280 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
294 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
281 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
295 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
282 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
296 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
283 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
297 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
284 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
298 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
285 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
299 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
286 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
300 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
287 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
301 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
288 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
302 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
289 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
303 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
290 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
304 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
291 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
305 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
292 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
306 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
293 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
307 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
294 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
308 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
295 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
309 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
296 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
310 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
297 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
311 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
298 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
312 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
299 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
313 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
300 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
314 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
301 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
315 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
302 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
316 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
303 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
317 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
304 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
318 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
305 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
319 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
306 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
320 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
307 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
321 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
308 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
322 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
309 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
323 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
310 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
324 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
311 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
325 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
312 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
326 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
313 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
327 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
314 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
328 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
315 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
329 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
316 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
330 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
317 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
331 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
318 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
332 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
319 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
333 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
320 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
334 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
321 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
335 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
322 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
336 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
323 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
337 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
324 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
338 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
325 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
339 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
326 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
340 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
327 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp} 1*}) |
341 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
328 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
342 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
329 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
343 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
330 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
344 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
331 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
345 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
332 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
346 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
333 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
347 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
334 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
348 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
335 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
349 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
336 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
350 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
337 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
351 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
338 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
352 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
339 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
353 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
340 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
354 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
341 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
355 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
342 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
356 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
343 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
357 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
344 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
358 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
345 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
359 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
346 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
360 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
347 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
361 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
348 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
362 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
349 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
363 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
350 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
364 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
351 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
365 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
352 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
366 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
353 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
367 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
354 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*}) |
368 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
355 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
369 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
356 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*}) |
370 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
357 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
371 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
358 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
372 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
359 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp} 1*}) |
373 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
360 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
374 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
361 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp} 1*}) |
375 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
362 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
376 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
363 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
377 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
364 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
378 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
365 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
379 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
366 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
380 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
367 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
381 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
368 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
382 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
369 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
383 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
370 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
384 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
371 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
385 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
372 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
386 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
373 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
387 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
374 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
388 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
375 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
389 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
376 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
390 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
377 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
391 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
378 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
392 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
379 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
393 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
380 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
394 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
381 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
395 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
382 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
396 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
383 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
397 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
384 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
398 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
385 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
399 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
386 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
400 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
387 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
401 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
388 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*}) |
402 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
389 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*}) |
403 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
390 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
404 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
391 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp} 1*}) |
405 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
392 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
406 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
393 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp} 1*}) |
407 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
394 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
408 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
395 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp} 1*}) |
409 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
396 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
410 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
397 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp} 1*}) |
411 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
398 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
412 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
399 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp} 1*}) |
413 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
400 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
414 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
401 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
415 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
402 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
416 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
403 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
417 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
404 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
418 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
405 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
419 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
406 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
420 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
407 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
421 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
408 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
422 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
409 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
423 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
410 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
424 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
411 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
425 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
412 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
426 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
413 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
427 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
414 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
428 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
415 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
429 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
416 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
430 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
417 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
431 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
418 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
432 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
419 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
433 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
420 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
434 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
421 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
435 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
422 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp} 1*}) |
436 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
423 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
437 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
424 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
438 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
425 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
439 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
426 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
440 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
427 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
441 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
428 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
442 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
429 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
443 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
430 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
444 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
431 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
445 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
432 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
446 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
433 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
447 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
434 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
448 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
435 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
449 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
436 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
450 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
437 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
451 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
438 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
452 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
439 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
453 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
440 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
454 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
441 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
455 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
442 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
456 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
443 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
457 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
444 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
458 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
445 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
459 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
446 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
460 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
447 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
461 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
448 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
462 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
449 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
463 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
450 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
464 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
451 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
465 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
452 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*}) |
466 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
453 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
467 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
454 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*}) |
468 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
455 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
469 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
456 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*}) |
470 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
457 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp} 1*}) |
471 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
458 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
472 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
459 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*}) |
473 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
460 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*}) |
474 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
461 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*}) |
475 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
462 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*}) |
476 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
463 done |
477 done |
464 |
478 |
465 print_quotients |
479 print_quotients |
466 |
480 |
467 end |
481 end |