2010-10-08 |
wenzelm |
more on ML antiquotations;
|
file |
diff |
annotate
|
2010-08-27 |
wenzelm |
proper context for various Thy_Output options, via official configuration options in ML and Isar;
|
file |
diff |
annotate
|
2010-07-27 |
wenzelm |
updated manual concerning theory loader;
|
file |
diff |
annotate
|
2010-05-31 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
2010-05-30 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
2010-05-18 |
wenzelm |
prefer structure Keyword and Parse;
|
file |
diff |
annotate
|
2010-04-16 |
wenzelm |
proper checking of ML functors (in Poly/ML 5.2 or later);
|
file |
diff |
annotate
|
2009-06-10 |
wenzelm |
eliminated escaped symbols;
|
file |
diff |
annotate
|
2009-05-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2009-03-09 |
wenzelm |
fornal markup for antiquotation options;
|
file |
diff |
annotate
|
2009-03-09 |
wenzelm |
moved @{ML_functor} and @{ML_text} to Pure;
|
file |
diff |
annotate
|
2009-03-09 |
wenzelm |
adapted ThyOutput.antiquotation;
|
file |
diff |
annotate
|
2009-03-08 |
wenzelm |
use simplified ThyOutput.antiquotation;
|
file |
diff |
annotate
|
2009-03-08 |
wenzelm |
adapted to structure Long_Name;
|
file |
diff |
annotate
|
2009-03-08 |
wenzelm |
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-02-26 |
wenzelm |
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
|
file |
diff |
annotate
|
2009-02-14 |
wenzelm |
clean_string/clean_name: proper treatment of \<dash>;
|
file |
diff |
annotate
|
2009-02-11 |
wenzelm |
added "inference" entity;
|
file |
diff |
annotate
|
2008-11-13 |
wenzelm |
ignore ThyOutput.source flag;
|
file |
diff |
annotate
|
2008-10-21 |
wenzelm |
ThyOutput: export some auxiliary operations;
|
file |
diff |
annotate
|
2008-09-29 |
haftmann |
added theory antiquotation
|
file |
diff |
annotate
|
2008-09-17 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
2008-09-16 |
wenzelm |
check setting and tool;
|
file |
diff |
annotate
|
2008-09-15 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
2008-09-15 |
wenzelm |
added formal markup for setting, executable, tool;
|
file |
diff |
annotate
|
2008-08-09 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
2008-06-25 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
2008-05-15 |
wenzelm |
tuned clean_name (underscore);
|
file |
diff |
annotate
|
2008-05-15 |
wenzelm |
clean_name: replace "_" by "-";
|
file |
diff |
annotate
|
2008-05-15 |
wenzelm |
clean_string: cover <;
|
file |
diff |
annotate
|
2008-05-14 |
wenzelm |
proper checking of various Isar elements;
|
file |
diff |
annotate
|
2008-05-08 |
wenzelm |
clean_string: map "_" to "\\_" (best used with underscore.sty);
|
file |
diff |
annotate
|
2008-05-07 |
wenzelm |
output_entity: ignore ThyOutput.source option;
|
file |
diff |
annotate
|
2008-05-05 |
wenzelm |
element: isakeyword markup;
|
file |
diff |
annotate
|
2008-05-02 |
wenzelm |
output_entity: added \mbox{} to prevent hyphenation;
|
file |
diff |
annotate
|
2008-05-02 |
wenzelm |
clean_string: handle { };
|
file |
diff |
annotate
|
2008-04-28 |
wenzelm |
proper command/keyword markup;
|
file |
diff |
annotate
|
2008-04-26 |
wenzelm |
added setup for Isar entities;
|
file |
diff |
annotate
|
2008-04-23 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
2008-04-17 |
wenzelm |
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
|
file |
diff |
annotate
|
2008-03-28 |
haftmann |
some styling
|
file |
diff |
annotate
|
2008-03-27 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
2008-03-24 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
2007-10-08 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
2007-09-15 |
haftmann |
fixed title
|
file |
diff |
annotate
|
2007-08-09 |
wenzelm |
adapted ThyLoad.check_thy;
|
file |
diff |
annotate
|
2007-07-19 |
berghofe |
Added named_thms antiquotation.
|
file |
diff |
annotate
|
2007-07-08 |
wenzelm |
renamed ML_exc to ML_exn;
|
file |
diff |
annotate
|
2007-02-10 |
haftmann |
added antiquotation for exceptions
|
file |
diff |
annotate
|
2007-01-19 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
file |
diff |
annotate
|
2007-01-19 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
2006-11-15 |
wenzelm |
Auxiliary antiquotations for Isabelle manuals.
|
file |
diff |
annotate
|