src/Pure/ex/Alternative_Headings.thy
Wed, 24 Nov 2021 15:33:43 +0100 wenzelm more uniform treatment of optional_argument for Latex elements;
Tue, 23 Nov 2021 21:02:13 +0100 wenzelm example: alternative document headings, based on more general document output markup;
less more (0) tip