equal
deleted
inserted
replaced
692 val (intrs', ctxt1) = |
692 val (intrs', ctxt1) = |
693 ctxt |> |
693 ctxt |> |
694 LocalTheory.notes kind |
694 LocalTheory.notes kind |
695 (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th], |
695 (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th], |
696 [Attrib.internal (K (ContextRules.intro_query NONE)), |
696 [Attrib.internal (K (ContextRules.intro_query NONE)), |
697 Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>> |
697 Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>> |
698 map (hd o snd); |
698 map (hd o snd); |
699 val (((_, elims'), (_, [induct'])), ctxt2) = |
699 val (((_, elims'), (_, [induct'])), ctxt2) = |
700 ctxt1 |> |
700 ctxt1 |> |
701 LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>> |
701 LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>> |
702 fold_map (fn (name, (elim, cases)) => |
702 fold_map (fn (name, (elim, cases)) => |