| 17 months ago ago |
disallow pending hyps;
|
file | diff | annotate |
| 21 months ago ago |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
|
file | diff | annotate |
| 22 months ago ago |
clarified signature;
|
file | diff | annotate |
| 22 months ago ago |
more operations;
|
file | diff | annotate |
| 2017-12-06 ago |
prefer control symbol antiquotations;
|
file | diff | annotate |
| 2016-12-13 ago |
more symbols;
|
file | diff | annotate |
| 2016-06-23 ago |
tuned signature;
|
file | diff | annotate |
| 2016-06-21 ago |
tuned;
|
file | diff | annotate |
| 2016-06-09 ago |
tuned signature;
|
file | diff | annotate |
| 2016-06-09 ago |
tuned;
|
file | diff | annotate |
| 2016-05-12 ago |
common entity definitions within a global or local theory context;
|
file | diff | annotate |
| 2016-04-28 ago |
unfold is subject to unfold_abs_def (still inactive);
|
file | diff | annotate |
| 2016-04-18 ago |
prefer internal attribute source;
|
file | diff | annotate |
| 2016-04-07 ago |
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
|
file | diff | annotate |
| 2016-04-05 ago |
clarified modules -- simplified bootstrap;
|
file | diff | annotate |
| 2016-04-01 ago |
removed redundant Position.set_range -- already done in Position.range;
|
file | diff | annotate |
| 2016-03-02 ago |
support for ML_exception_debugger;
|
file | diff | annotate |
| 2015-12-15 ago |
unused;
|
file | diff | annotate |
| 2015-12-09 ago |
tuned;
|
file | diff | annotate |
| 2015-12-09 ago |
unused;
|
file | diff | annotate |
| 2015-12-09 ago |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file | diff | annotate |
| 2015-10-30 ago |
tuned signature -- clarified modules;
|
file | diff | annotate |
| 2015-10-18 ago |
tuned signature;
|
file | diff | annotate |
| 2015-09-25 ago |
moved remaining display.ML to more_thm.ML;
|
file | diff | annotate |
| 2015-07-17 ago |
proper attribute;
|
file | diff | annotate |
| 2015-05-03 ago |
tuned output;
|
file | diff | annotate |
| 2015-05-03 ago |
tuned output -- avoid empty quites and extra breaks;
|
file | diff | annotate |
| 2015-04-03 ago |
more uniform "verbose" option to print name space;
|
file | diff | annotate |
| 2014-11-30 ago |
more abstract type Input.source;
|
file | diff | annotate |
| 2014-11-12 ago |
more careful ML source positions, for improved PIDE markup;
|
file | diff | annotate |
| 2014-11-11 ago |
more careful ML source positions, for improved PIDE markup;
|
file | diff | annotate |
| 2014-11-11 ago |
more position information, e.g. relevant for errors in generated ML source;
|
file | diff | annotate |
| 2014-11-07 ago |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file | diff | annotate |
| 2014-11-05 ago |
explicit type Keyword.keywords;
|
file | diff | annotate |
| 2014-11-01 ago |
tuned signature (see ab2483fad861);
|
file | diff | annotate |
| 2014-08-27 ago |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
file | diff | annotate |
| 2014-08-25 ago |
tuned signature;
|
file | diff | annotate |
| 2014-08-21 ago |
tuned signature -- define some elementary operations earlier;
|
file | diff | annotate |
| 2014-08-21 ago |
tuned;
|
file | diff | annotate |
| 2014-08-19 ago |
tuned signature -- moved type src to Token, without aliases;
|
file | diff | annotate |
| 2014-08-14 ago |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file | diff | annotate |
| 2014-08-14 ago |
localized command 'method_setup' and 'attribute_setup';
|
file | diff | annotate |
| 2014-08-14 ago |
tuned;
|
file | diff | annotate |
| 2014-08-14 ago |
tuned;
|
file | diff | annotate |
| 2014-08-14 ago |
tuned signature;
|
file | diff | annotate |
| 2014-08-13 ago |
localized attribute definitions;
|
file | diff | annotate |
| 2014-08-05 ago |
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
|
file | diff | annotate |
| 2014-04-06 ago |
more source positions;
|
file | diff | annotate |
| 2014-04-06 ago |
more source positions;
|
file | diff | annotate |
| 2014-03-31 ago |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file | diff | annotate |
| 2014-03-27 ago |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file | diff | annotate |
| 2014-03-25 ago |
proper configuration option "ML_print_depth";
|
file | diff | annotate |
| 2014-03-25 ago |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file | diff | annotate |
| 2014-03-25 ago |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file | diff | annotate |
| 2014-03-24 ago |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file | diff | annotate |
| 2014-03-14 ago |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file | diff | annotate |
| 2014-03-11 ago |
tuned signature;
|
file | diff | annotate |
| 2014-03-10 ago |
more markup;
|
file | diff | annotate |
| 2014-03-10 ago |
clarified Args.check_src: retain name space information for error output;
|
file | diff | annotate |
| 2014-03-10 ago |
clarified Args.src: more abstract type, position refers to name only;
|
file | diff | annotate |