equal
deleted
inserted
replaced
185 |-> (fn intross => LocalTheory.note Thm.theoremK |
185 |-> (fn intross => LocalTheory.note Thm.theoremK |
186 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
186 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
187 |>> snd |
187 |>> snd |
188 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
188 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
189 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
189 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
190 [Attrib.internal (K (RuleCases.case_names case_names)), |
190 [Attrib.internal (K (Rule_Cases.case_names case_names)), |
191 Attrib.internal (K (RuleCases.consumes 1)), |
191 Attrib.internal (K (Rule_Cases.consumes 1)), |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
193 (preds ~~ inducts)) #>> maps snd) |
193 (preds ~~ inducts)) #>> maps snd) |
194 |> snd |
194 |> snd |
195 end |
195 end |
196 (* @end *) |
196 (* @end *) |