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 signature;
2014-11-30, by wenzelm
tuned signature;
2014-11-30, by wenzelm
tuned signature -- prefer Input.source;
2014-11-30, by wenzelm
more abstract type Input.source;
2014-11-30, by wenzelm
encode text with control symbols;
2014-11-29, by wenzelm
proper HTML.encode;
2014-11-29, by wenzelm
prefer abbrev for is_unit
2014-11-26, by haftmann
do not conceal inductive predicate names properly, following 4a3747517552
2014-11-26, by haftmann
tuned
2014-11-26, by haftmann
renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26, by wenzelm
added ML antiquotation @{apply n} or @{apply n(k)};
2014-11-26, by wenzelm
even more exception traces for Document.update, which goes through additional execution wrappers;
2014-11-26, by wenzelm
more informative failure of protocol commands, with exception trace;
2014-11-26, by wenzelm
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-11-26, by wenzelm
tuned proof that pmfs are bnfs
2014-11-25, by hoelzl
projections of pair_pmf (by D. Traytel)
2014-11-25, by hoelzl
merged
2014-11-24, by wenzelm
removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
2014-11-24, by wenzelm
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
2014-11-24, by traytel
add congruence solver to measurability prover
2014-11-24, by hoelzl
cleanup measurability prover
2014-11-24, by hoelzl
updated SMT certificates
2014-11-24, by blanchet
added one more CVC4 option that helps Judgment Day (10 theory version)
2014-11-24, by blanchet
tuned whitespace
2014-11-24, by blanchet
keep all 'ctr' theorems
2014-11-24, by blanchet
smoothly handle unit codatatypes in 'primcorec'
2014-11-24, by blanchet
careful with de Bruijn indices
2014-11-24, by blanchet
improved message in 'co' case
2014-11-24, by blanchet
updated NEWS
2014-11-24, by blanchet
no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)
2014-11-24, by blanchet
added Z3 reconstruction rule suggested by F. Maric
2014-11-24, by blanchet
one more CVC4 option that helps
2014-11-24, by blanchet
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
2014-11-24, by blanchet
update CVC4 version docs
2014-11-24, by blanchet
tuned signature;
2014-11-22, by wenzelm
tuned;
2014-11-22, by wenzelm
misc tuning and modernization;
2014-11-22, by wenzelm
misc tuning and modernization;
2014-11-22, by wenzelm
more careful ML source positions, for improved PIDE markup;
2014-11-22, by wenzelm
named_theorems: multiple args;
2014-11-22, by wenzelm
tuned;
2014-11-21, by wenzelm
removed some add-ons from modules that are relevant for the inference kernel;
2014-11-21, by wenzelm
add lemma following a proof suggestion by Joachim Breitner
2014-11-21, by Andreas Lochbihler
add lemma
2014-11-21, by Andreas Lochbihler
register pmf as BNF
2014-11-21, by Andreas Lochbihler
added CVC4 option that helps on JD
2014-11-20, by blanchet
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
2014-11-20, by blanchet
work around bug in CVC4, with boolean arguments to (co)datatypes
2014-11-20, by blanchet
other way of crashing (with CVC4)
2014-11-20, by blanchet
set right logic for CVC4 with (co)datatypes
2014-11-20, by blanchet
removed explicit '--quant-cf' option to CVC4, now that it's the default
2014-11-20, by blanchet
more accurate lemma name
2014-11-19, by traytel
parse CVC4 unsat cores
2014-11-19, by blanchet
tuning
2014-11-19, by blanchet
removed redundant code line
2014-11-19, by blanchet
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
2014-11-18, by wenzelm
add reindex rules for distr and nn_integral on count_space
2014-11-17, by hoelzl
generalized lemmas and tuned proofs
2014-11-17, by haftmann
generalized lemmas (particularly concerning dvd) as far as appropriate
2014-11-17, by haftmann
formally self-contained gcd type classes
2014-11-17, by haftmann

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

isabelle