equal
deleted
inserted
replaced
357 (* definition of alpha-distinct lemmas *) |
357 (* definition of alpha-distinct lemmas *) |
358 val _ = warning "Distinct theorems"; |
358 val _ = warning "Distinct theorems"; |
359 val (alpha_distincts, alpha_bn_distincts) = |
359 val (alpha_distincts, alpha_bn_distincts) = |
360 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
360 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
361 |
361 |
362 (* definition of raw_alpha_eq_iff lemmas *) |
362 (* definition of alpha_eq_iff lemmas *) |
|
363 (* they have a funny shape for the simplifier *) |
363 val _ = warning "Eq-iff theorems"; |
364 val _ = warning "Eq-iff theorems"; |
364 val alpha_eq_iff = |
365 val alpha_eq_iff = |
365 if get_STEPS lthy > 5 |
366 if get_STEPS lthy > 5 |
366 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
367 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
367 else raise TEST lthy4 |
368 else raise TEST lthy4 |
468 val qfv_bns = map #qconst qfv_bns_info |
469 val qfv_bns = map #qconst qfv_bns_info |
469 |
470 |
470 (* respectfulness proofs *) |
471 (* respectfulness proofs *) |
471 |
472 |
472 (* HERE *) |
473 (* HERE *) |
|
474 |
|
475 val (_, lthy8') = lthy8 |
|
476 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
|
477 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
|
478 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
|
479 ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs) |
|
480 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
|
481 |
473 |
482 |
474 val _ = |
483 val _ = |
475 if get_STEPS lthy > 16 |
484 if get_STEPS lthy > 16 |
476 then true else raise TEST lthy8 |
485 then true else raise TEST lthy8' |
477 |
486 |
478 (* old stuff *) |
487 (* old stuff *) |
479 |
488 |
480 val _ = warning "Proving respects"; |
489 val _ = warning "Proving respects"; |
481 |
490 |