equal
deleted
inserted
replaced
717 Spec_Rules.add |
717 Spec_Rules.add |
718 (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |> |
718 (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |> |
719 Local_Theory.notes |
719 Local_Theory.notes |
720 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ |
720 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ |
721 map (fn th => [([th], |
721 map (fn th => [([th], |
722 [Attrib.internal (K (Context_Rules.intro_query NONE)), |
722 [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>> |
723 Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>> |
|
724 map (hd o snd); |
723 map (hd o snd); |
725 val (((_, elims'), (_, [induct'])), lthy2) = |
724 val (((_, elims'), (_, [induct'])), lthy2) = |
726 lthy1 |> |
725 lthy1 |> |
727 Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> |
726 Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> |
728 fold_map (fn (name, (elim, cases, k)) => |
727 fold_map (fn (name, (elim, cases, k)) => |