equal
deleted
inserted
replaced
37 |
37 |
38 notation |
38 notation |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
41 thm alpha_rtrm1_alpha_bp.intros |
41 thm alpha_rtrm1_alpha_bp.intros |
42 thm fv_rtrm1_fv_bp.simps |
42 thm fv_rtrm1_fv_bp.simps[no_vars] |
43 |
43 |
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
45 thm alpha1_inj |
45 thm alpha1_inj |
46 |
46 |
47 local_setup {* |
47 local_setup {* |