src/Doc/Implementation/Logic.thy
18 months ago wenzelm 2017-12-06 more embedded cartouche arguments; more uniform LaTeX output for control symbols;
2017-04-09 wenzelm 2017-04-09 tuned signature -- prefer qualified names;
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-09 wenzelm 2016-04-09 clarified context; avoid Unsynchronized.ref;
2016-02-19 wenzelm 2016-02-19 moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
2015-12-29 wenzelm 2015-12-29 eliminated obscure macro that is in conflict with amsmath.sty;
2015-12-16 wenzelm 2015-12-16 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 more uniform jEdit properties;
2015-11-04 wenzelm 2015-11-04 more antiquotations;
2015-10-22 wenzelm 2015-10-22 more control symbols; tuned;
2015-10-20 wenzelm 2015-10-20 isabelle update_cartouches -t;
2015-10-18 wenzelm 2015-10-18 more control symbols;
2015-10-16 wenzelm 2015-10-16 Markdown support in document text;
2015-10-14 wenzelm 2015-10-14 more symbols;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-04-01 wenzelm 2015-04-01 misc tuning -- keep name space more clean;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-10-20 wenzelm 2014-10-20 tuned spacing;
2014-10-07 wenzelm 2014-10-07 more cartouches;
2014-10-05 wenzelm 2014-10-05 prefer @{cite} antiquotation;
2014-04-15 wenzelm 2014-04-15 tuned spelling;
2014-04-05 haftmann 2014-04-05 closer correspondence of document and session names, while maintaining document names for external reference