| 2011-06-27 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| 2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 2010-09-20 |
haftmann |
adjusted
|
file |
diff |
annotate
|
| 2010-09-16 |
haftmann |
moved material intro distribution proper
|
file |
diff |
annotate
|
| 2010-09-13 |
haftmann |
'class' and 'type' are now antiquoations by default
|
file |
diff |
annotate
|
| 2010-08-31 |
haftmann |
allow explicit parameter for code width
|
file |
diff |
annotate
|
| 2010-08-31 |
haftmann |
distinguish code production and code presentation
|
file |
diff |
annotate
|
| 2010-08-31 |
haftmann |
dropped legacy interfaces
|
file |
diff |
annotate
|
| 2010-08-30 |
haftmann |
tuned
|
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-05-31 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| 2010-05-08 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| 2010-03-14 |
wenzelm |
localized @{class} and @{type};
|
file |
diff |
annotate
|
| 2010-02-20 |
haftmann |
adjusted to changes in cs b987b803616d
|
file |
diff |
annotate
|
| 2010-01-14 |
haftmann |
adjusted to changes in code equation administration
|
file |
diff |
annotate
|
| 2009-12-11 |
haftmann |
option width for Code_Target.code_of
|
file |
diff |
annotate
|
| 2009-06-24 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| 2009-05-14 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| 2009-05-14 |
haftmann |
adapted code tutorial to recent changes in code
|
file |
diff |
annotate
|
| 2009-04-25 |
haftmann |
adjusted to change in code_wellsorted.ML
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
moved @{ML_functor} and @{ML_text} to Pure;
|
file |
diff |
annotate
|
| 2009-03-02 |
haftmann |
reduced confusion code_funcgr vs. code_wellsorted
|
file |
diff |
annotate
|
| 2009-02-11 |
haftmann |
display code theorems with HOL equality
|
file |
diff |
annotate
|
| 2009-01-23 |
haftmann |
be more liberal with selected code statements
|
file |
diff |
annotate
|
| 2009-01-08 |
haftmann |
dded code_thm antiquotation
|
file |
diff |
annotate
|
| 2008-12-01 |
haftmann |
consider TeX spacing conventions for punctuation marks
|
file |
diff |
annotate
|
| 2008-11-10 |
haftmann |
clarified verbatim vs. typewriter
|
file |
diff |
annotate
|
| 2008-11-03 |
haftmann |
improved verbatim mechanism
|
file |
diff |
annotate
|
| 2008-10-24 |
haftmann |
explicit namings for generated code
|
file |
diff |
annotate
|
| 2008-10-17 |
haftmann |
added type antiquotation
|
file |
diff |
annotate
|
| 2008-10-02 |
haftmann |
corrected class antiquotation
|
file |
diff |
annotate
|
| 2008-10-01 |
haftmann |
added more_antiquote.ML
|
file |
diff |
annotate
|