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 whitespace
2016-03-22, by blanchet
compile
2016-03-22, by blanchet
added 'corec' examples and tests
2016-03-22, by blanchet
file header
2016-03-22, by blanchet
added two 'corec' examples
2016-03-22, by blanchet
document addition of 'corec'
2016-03-22, by blanchet
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-22, by blanchet
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-03-22, by blanchet
nicer error
2016-03-22, by blanchet
more debugging
2016-03-22, by blanchet
more general, reliable N2M
2016-03-22, by blanchet
better warning, with definitions in right order
2016-03-22, by blanchet
export ML function
2016-03-22, by blanchet
added timers to N2M
2016-03-22, by blanchet
document that n2m does not depend on most things in fp_sugar in its type
2016-03-22, by traytel
clarified rule structure;
2016-03-21, by wenzelm
accomodate Isabelle identifiers with subscripts;
2016-03-21, by wenzelm
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
2016-03-21, by wenzelm
eliminated unused argument (see also 58110c1e02bc);
2016-03-21, by wenzelm
add le_log_of_power and le_log2_of_power by Tobias Nipkow
2016-03-21, by hoelzl
unified CHAR with CHR syntax
2016-03-19, by haftmann
isabelle process -T THEORY;
2016-03-18, by wenzelm
proper option -l;
2016-03-18, by wenzelm
avoid redundant addLeftOfScrollBar;
2016-03-18, by wenzelm
no dependency on HighlightPlugin, despite e7b2cfcef94c;
2016-03-18, by wenzelm
observe ML print depth;
2016-03-18, by wenzelm
clarified print depth;
2016-03-18, by wenzelm
recovered from Unicode accident in 7248d106c607;
2016-03-18, by wenzelm
merged
2016-03-18, by wenzelm
tuned -- fewer warnings;
2016-03-18, by wenzelm
discontinued slightly odd "secure" mode;
2016-03-18, by wenzelm
clarified Pretty.T toplevel pp;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
tuned header;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
@{make_string} is available during Pure bootstrap;
2016-03-17, by wenzelm
clarified modules;
2016-03-17, by wenzelm
unused;
2016-03-17, by wenzelm
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned signature;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned whitespace;
2016-03-17, by wenzelm
proper ML type;
2016-03-17, by wenzelm
merged
2016-03-18, by Andreas Lochbihler
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-18, by Andreas Lochbihler
superfluous premise (noticed by Julian Nagele)
2016-03-18, by nipkow
added tree lemmas
2016-03-18, by nipkow
normalize schematic names since they are used to instantiate the theorem later
2016-03-18, by traytel
more stuff for extended nonnegative real numbers
2016-03-17, by hoelzl
less preconditions
2016-03-17, by Andreas Lochbihler
merged
2016-03-16, by wenzelm
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16, by wenzelm
pro-forma selection for improved error message;
2016-03-16, by wenzelm
eliminated without magic name;
2016-03-16, by wenzelm
NEWS;
2016-03-16, by wenzelm
always build with full results;
2016-03-16, by wenzelm
clarified name;
2016-03-16, by wenzelm
isabelle process -d;
2016-03-16, by wenzelm

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

isabelle