isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 tip

tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: name according to db model without Sessions.Structure/Deps;
20 months ago, by wenzelm
added lemmas
20 months ago, by nipkow
tuned
20 months ago, by nipkow
spelling;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
read theory with PIDE markup from session database;
20 months ago, by wenzelm
clarified signature: provide XZ.Cache where Export.Entry is created;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified exports;
20 months ago, by wenzelm
clarified markup (refining 1c59b555ac4a);
20 months ago, by wenzelm
clarified markup: support more completion, e.g. within ROOTS;
20 months ago, by wenzelm
more accurate markup (refining 1c59b555ac4a);
20 months ago, by wenzelm
tuned signature --- more operations;
20 months ago, by wenzelm
clarified File_Format.detect: needs to operate on full node name;
20 months ago, by wenzelm
more accurate syntax, following Sessions.parse_roots in Scala;
20 months ago, by wenzelm
PIDE support for session ROOTS;
20 months ago, by wenzelm
more robust;
20 months ago, by wenzelm
more Unicode;
20 months ago, by wenzelm
eliminated odd "Read_me";
20 months ago, by wenzelm
eliminated odd "Read_me";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
20 months ago, by wenzelm
moved some lemmas from AFP to distribution
20 months ago, by haftmann
avoid duplicate entries: snippet_command is defined within node;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
proper span position for blobs in batch-build (but: practically irrelevant);
20 months ago, by wenzelm
proper treatment of singleton Position.Offset within blob (amending cb9d5af781b4);
20 months ago, by wenzelm
more robust batch-build;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature, notably access to blob files;
20 months ago, by wenzelm
support for PIDE markup for auxiliary files ("blobs");
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature --- more explicit types;
20 months ago, by wenzelm
merged
20 months ago, by Peter Lammich
removed session name
20 months ago, by Peter Lammich
merged
20 months ago, by nipkow
NEWS
20 months ago, by nipkow
merged
20 months ago, by Peter Lammich
summarized structural and ordering invariant for trees
20 months ago, by Peter Lammich
Total correctness examples by Walter Guttmann
20 months ago, by nipkow
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
20 months ago, by nipkow
tuned
20 months ago, by nipkow
Highlight that 'intro_locales' and 'trace_locales' are useful debug features, plus minor clarifications.
20 months ago, by ballarin
merged
20 months ago, by nipkow
added abbrev
20 months ago, by nipkow
merged
20 months ago, by wenzelm
clarified signature --- more positions;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned proof preplay to explicitly refer to Z3 backend
20 months ago, by desharna
A bunch of suggestions from Pedro Sánchez Terraf
20 months ago, by paulson
merged
20 months ago, by paulson

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 tip

isabelle