src/Pure/ex/Alternative_Headings_Examples.thy
Tue, 23 Nov 2021 21:02:13 +0100 wenzelm example: alternative document headings, based on more general document output markup;
less more (0) tip