src/HOL/ex/Cartouche_Examples.thy
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Wed, 12 Mar 2014 22:57:50 +0100 wenzelm tuned signature -- clarified module name;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Sat, 25 Jan 2014 13:55:09 +0100 wenzelm simplified inner syntax;
Wed, 22 Jan 2014 15:28:19 +0100 wenzelm avoid breakdown of document preparation, which does not understand cartouche tokens yet;
Wed, 22 Jan 2014 15:11:10 +0100 wenzelm more cartouche examples, including uniform nesting of sub-languages;
Sun, 19 Jan 2014 21:33:45 +0100 wenzelm implicit "cartouche" method (experimental, undocumented);
Sun, 19 Jan 2014 21:00:42 +0100 wenzelm more examples;
Sat, 18 Jan 2014 19:35:42 +0100 wenzelm proper \<newline>;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
less more (0) tip