equal
deleted
inserted
replaced
281 alpha_bn_names = alpha_bn_names, |
281 alpha_bn_names = alpha_bn_names, |
282 alpha_bn_trms = alpha_bn_trms, |
282 alpha_bn_trms = alpha_bn_trms, |
283 alpha_bn_tys = alpha_bn_tys, |
283 alpha_bn_tys = alpha_bn_tys, |
284 alpha_intros = alpha_intros, |
284 alpha_intros = alpha_intros, |
285 alpha_cases = alpha_cases, |
285 alpha_cases = alpha_cases, |
286 alpha_raw_induct = alpha_raw_induct}, lthy') |
286 alpha_raw_induct = alpha_raw_induct}, Local_Theory.restore lthy') |
287 end |
287 end |
288 |
288 |
289 |
289 |
290 (** induction proofs **) |
290 (** induction proofs **) |
291 |
291 |