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 +10000 tip

tuned syntax -- more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
prefer symbols;
2015-10-10, by wenzelm
use Isabelle symbols by default;
2015-10-10, by wenzelm
isabelle update_cartouches;
2015-10-10, by wenzelm
more explicit HTML.symbols;
2015-10-10, by wenzelm
NEWS;
2015-10-09, by wenzelm
more direct HTML presentation, without print mode;
2015-10-09, by wenzelm
discontinued specific HTML syntax;
2015-10-09, by wenzelm
installable TTF for MS IE 9+;
2015-10-09, by wenzelm
output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-10-09, by wenzelm
tuned output;
2015-10-09, by wenzelm
server-side fonts;
2015-10-09, by wenzelm
more accurate imitation of "cp -p -f";
2015-10-09, by wenzelm
more Present operations on Scala side;
2015-10-09, by wenzelm
clarified, according to Isabelle_System.copy_file in ML;
2015-10-09, by wenzelm
NEWS
2015-10-09, by kuncar
documentation for transfer debug methods
2015-10-09, by kuncar
add a file with examples of debugging transfer
2015-10-09, by kuncar
new methods for debugging transfer and transfer_prover
2015-10-09, by kuncar
right parenthesization
2015-10-09, by kuncar
made TPTP SZS status more compliant
2015-10-08, by blanchet
tuning
2015-10-08, by blanchet
measurable sets on product spaces are embeddings of countable products
2015-10-08, by hoelzl
generalize eqI theorems for product measures
2015-10-08, by hoelzl
isabelle update_cartouches;
2015-10-07, by wenzelm
more glyphs from DejaVuSansMono and DejaVuSansMono-Bold: 0100-017F Latin Extended-A, 0180-024F Latin Extended-B;
2015-10-07, by wenzelm
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-10-07, by hoelzl
avoid 'legacy binding' warning
2015-10-07, by blanchet
removed dead code
2015-10-07, by blanchet
merged
2015-10-07, by wenzelm
back to old-fashioned GC, which appears to work better with interactive applications;
2015-10-07, by wenzelm
routine check of theory context;
2015-08-31, by wenzelm
proper context;
2015-10-06, by wenzelm
proper context;
2015-10-06, by wenzelm
clarify docs
2015-10-07, by blanchet
updated docs
2015-10-07, by blanchet
made documentation more accurate
2015-10-07, by blanchet
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
2015-10-07, by blanchet
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
2015-10-06, by blanchet
parallel tests: 6h & 12h;
2015-10-06, by wenzelm
news
2015-10-06, by blanchet
generate 'case_transfer' unconditionally
2015-10-06, by blanchet
isabelle update_cartouches;
2015-10-06, by wenzelm
isabelle update_cartouches;
2015-10-06, by wenzelm
merged
2015-10-06, by wenzelm
avoid hardwired frees;
2015-10-06, by wenzelm
added Thm.forall_intr_name;
2015-10-06, by wenzelm
added 'proposition' command;
2015-10-06, by wenzelm
fewer aliases for toplevel theorem statements;
2015-10-06, by wenzelm
just one theorem kind, which is legacy anyway;
2015-10-06, by wenzelm
pretty_const: proper local name space;
2015-10-06, by wenzelm
collect the names from goals in favor of fragile exports
2015-10-06, by traytel
compile
2015-10-06, by blanchet
tuning
2015-10-06, by blanchet
avoid legacy syntax
2015-10-06, by blanchet
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
2015-10-05, by blanchet
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
2015-10-05, by blanchet

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

isabelle