| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/ex/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 954 B |
|
Quelle Alternative_Headings.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Pure/ex/Alternative_Headings.thy Author: Makarius *) chapter ‹Alternative document headings› theory Alternative_Headings imports Pure keywords "chapter*" "section*" "subsection*" "subsubsection*" :: document_heading begin ML ‹ local fun alternative_heading name body = [XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argumen fun document_heading (name, pos) = Outer_Syntax.command (name, pos) (name ^ " heading") (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") > Document_Output.document_output {markdown = false, markup = alternative_heading name}); val _ = List.app document_heading [🍋‹chapter*›, 🍋‹section*›, 🍋‹subsection*›, 🍋‹subsubsection*›]; in end› end
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-05-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26