src/HOL/ex/Cartouche_Examples.thy
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 09 Apr 2014 20:58:32 +0200 wenzelm proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
Wed, 09 Apr 2014 17:54:09 +0200 wenzelm allow text cartouches in regular outer syntax categories "text" and "altstring";
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