2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-06 wenzelm 2015-04-06 tuned;
2015-04-06 wenzelm 2015-04-06 clarified rail syntax;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-06 wenzelm 2015-04-06 clarified command keyword markup;
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-04-06 wenzelm 2015-04-06 allow prefix before keyword, notably 'private';
2015-04-06 wenzelm 2015-04-06 support local command setup;
2015-04-06 wenzelm 2015-04-06 proper header; misc tuning;
2015-04-06 wenzelm 2015-04-06 tuned signature;
2015-04-06 wenzelm 2015-04-06 tuned;
2015-04-06 nipkow 2015-04-06 new theory Library/Tree_Multiset.thy
2015-04-04 wenzelm 2015-04-04 more standard local_theory command setup;
2015-04-04 wenzelm 2015-04-04 some explanation of 'private';
2015-04-04 wenzelm 2015-04-04 tuned message;
2015-04-04 wenzelm 2015-04-04 more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
2015-04-04 wenzelm 2015-04-04 support private scope for individual local theory commands; tuned signature;
2015-04-03 wenzelm 2015-04-03 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
2015-04-03 wenzelm 2015-04-03 obsolete (see 8b7caf447357);
2015-04-03 wenzelm 2015-04-03 check wrt. proper context, e.g. relevant for 'experiment' target;
2015-04-03 wenzelm 2015-04-03 clarified name space policy: show less stuff in usual print functions;
2015-04-03 wenzelm 2015-04-03 unused;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-04-03 wenzelm 2015-04-03 tuned;
2015-04-02 wenzelm 2015-04-02 merged
2015-04-02 wenzelm 2015-04-02 proper treatment of internal method name as already checked Token.src;
2015-04-02 wenzelm 2015-04-02 tuned signature;
2015-04-02 wenzelm 2015-04-02 export for informative purposes;
2015-04-02 haftmann 2015-04-02 sort constraints are inherent part of class abbreviations (in contrast to class constants)
2015-04-02 haftmann 2015-04-02 semidom contains distributive minus, by convention
2015-04-02 wenzelm 2015-04-02 clarified method_closure; added option for Eisbach, which makes its own closure;
2015-04-02 wenzelm 2015-04-02 operation on embedded sources for Eisbach;
2015-04-02 wenzelm 2015-04-02 tuned signature;
2015-04-02 wenzelm 2015-04-02 tuned -- emphasize semantics of already checked src;
2015-04-01 wenzelm 2015-04-01 misc tuning -- keep name space more clean;
2015-04-01 wenzelm 2015-04-01 tuned;
2015-04-01 wenzelm 2015-04-01 merged
2015-04-01 wenzelm 2015-04-01 misc tuning -- keep name space more clean;
2015-04-01 wenzelm 2015-04-01 added command 'experiment';
2015-04-01 wenzelm 2015-04-01 imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;
2015-04-01 wenzelm 2015-04-01 NEWS;
2015-04-01 wenzelm 2015-04-01 clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
2015-04-01 wenzelm 2015-04-01 evade popular keyword;
2015-04-01 wenzelm 2015-04-01 tuned signature;
2015-04-01 wenzelm 2015-04-01 clarified module; more parallel processing;
2015-04-01 wenzelm 2015-04-01 ISABELLE_JAVA_SYSTEM_OPTIONS for scala REPL;
2015-04-01 wenzelm 2015-04-01 more reactive interrupts;
2015-04-01 wenzelm 2015-04-01 added isabelle build option -x, to exclude sessions;
2015-04-01 wenzelm 2015-04-01 added isabelle build option -k, for fast off-line checking of theory sources;
2015-04-01 wenzelm 2015-04-01 tuned signature;
2015-04-01 wenzelm 2015-04-01 tuned message;
2015-04-01 wenzelm 2015-04-01 tuned signature;
2015-03-31 wenzelm 2015-03-31 more visibility flags on background naming;
2015-03-31 wenzelm 2015-03-31 support for explicit scope of private entries;
2015-03-31 wenzelm 2015-03-31 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-31 wenzelm 2015-03-31 tuned -- avoid exotic Name_Space.defined_entry;
2015-03-31 wenzelm 2015-03-31 tuned;