src/CTT/CTT.thy
2017-04-09 wenzelm 2017-04-09 clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;
2017-03-23 wenzelm 2017-03-23 tuned proof;
2017-02-03 wenzelm 2017-02-03 misc tuning;
2016-07-15 wenzelm 2016-07-15 misc tuning and modernization; proper document setup;
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2015-10-10 wenzelm 2015-10-10 tuned syntax -- more symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-20 wenzelm 2014-12-20 proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
2014-11-11 wenzelm 2014-11-11 more symbols;
2014-11-11 wenzelm 2014-11-11 tuned whitespace;
2014-11-11 wenzelm 2014-11-11 more markup;
2014-11-11 wenzelm 2014-11-11 more Isar proof methods;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2008-05-18 wenzelm 2008-05-18 setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-03-25 wenzelm 2008-03-25 more antiquotations;
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-06-02 wenzelm 2006-06-02 removed obsolete ML files;
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-09-16 wenzelm 2005-09-16 converted to Isar theory format;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-21 wenzelm 2004-05-21 proper use of 'syntax';
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2000-11-14 paulson 2000-11-14 x-symbol support for Pi, Sigma, -->, : (membership) note that "lam" is displayed as TWO lambda-symbols
1997-10-10 wenzelm 1997-10-10 fixed dots;
1995-06-21 clasohm 1995-06-21 removed \...\ inside strings
1994-03-17 lcp 1994-03-17 new type declaration syntax instead of numbers
1993-10-04 wenzelm 1993-10-04 replaced id by idt; added parse rules for --> and *; removed ndependent_tr;
1993-09-16 clasohm 1993-09-16 Initial revision