#
d085e5b3 |
|
03-Dec-2019 |
wenzelm <none@none> |
more operations;
|
#
e17e9363 |
|
20-Oct-2019 |
wenzelm <none@none> |
clarified signature: name of standard_proof is authentic, otherwise empty;
|
#
050e1531 |
|
17-Oct-2019 |
wenzelm <none@none> |
support dummy term;
|
#
8e0ec923 |
|
12-Oct-2019 |
wenzelm <none@none> |
clarified signature default;
|
#
173afba1 |
|
12-Oct-2019 |
wenzelm <none@none> |
clarified signature default;
|
#
24212eb9 |
|
12-Oct-2019 |
wenzelm <none@none> |
more operations for type classes;
|
#
e5105177 |
|
12-Oct-2019 |
wenzelm <none@none> |
clarified output and input of Typ/Term;
|
#
0ba6f50c |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified oracle_proof;
|
#
ec801e15 |
|
04-Oct-2019 |
wenzelm <none@none> |
obsolete;
|
#
3dbd8fa2 |
|
04-Oct-2019 |
wenzelm <none@none> |
Term_XML.Encode/Decode.term uses Const "typargs";
|
#
a8d425ee |
|
17-Aug-2019 |
wenzelm <none@none> |
clarified type for recorded oracles;
|
#
2a1a9b9c |
|
17-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
cbd5363d |
|
15-Aug-2019 |
wenzelm <none@none> |
clarified PThm: theory_name simplifies retrieval from exports;
|
#
2a1c4073 |
|
15-Aug-2019 |
wenzelm <none@none> |
Indexname.toString according to string_of_vname' in ML;
|
#
b032ab44 |
|
15-Aug-2019 |
wenzelm <none@none> |
clarified type Indexname, with plain value Int; eliminated pointless cache_int;
|
#
a50b1dda |
|
15-Aug-2019 |
wenzelm <none@none> |
more complete pattern match;
|
#
263629fb |
|
15-Aug-2019 |
wenzelm <none@none> |
support for (fully reconstructed) proof terms in Scala; proper cache_typs;
|
#
35c5e2c7 |
|
20-Jul-2019 |
wenzelm <none@none> |
more operations: support type classes within the logic;
|
#
6dd4eace |
|
20-Jul-2019 |
wenzelm <none@none> |
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
|
#
a370b4a1 |
|
24-May-2018 |
wenzelm <none@none> |
more general cache, also for term substructures;
|
#
57494739 |
|
12-Jul-2011 |
wenzelm <none@none> |
more uniform Term and Term_XML modules;
|
#
9e1645ff |
|
12-Jul-2011 |
wenzelm <none@none> |
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
|
#
a33bb41d |
|
12-Jul-2011 |
wenzelm <none@none> |
tuned XML modules;
|
#
dada9359 |
|
10-Jul-2011 |
wenzelm <none@none> |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
|
#
be8a0acb |
|
10-Jul-2011 |
wenzelm <none@none> |
lambda terms with XML data representation in Scala; avoid `class` in signature;
|