equal
deleted
inserted
replaced
701 val (intrs', ctxt1) = |
701 val (intrs', ctxt1) = |
702 ctxt |> |
702 ctxt |> |
703 LocalTheory.notes kind |
703 LocalTheory.notes kind |
704 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], |
704 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], |
705 [Attrib.internal (K (ContextRules.intro_query NONE)), |
705 [Attrib.internal (K (ContextRules.intro_query NONE)), |
706 Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>> |
706 Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>> |
707 map (hd o snd); |
707 map (hd o snd); |
708 val (((_, elims'), (_, [induct'])), ctxt2) = |
708 val (((_, elims'), (_, [induct'])), ctxt2) = |
709 ctxt1 |> |
709 ctxt1 |> |
710 LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> |
710 LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> |
711 fold_map (fn (name, (elim, cases)) => |
711 fold_map (fn (name, (elim, cases)) => |