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

code for while directly, not via while_option
2012-11-04, by nipkow
executable true liveness analysis incl an approximating version
2012-11-04, by nipkow
now that sets are executable again, no more special treatment of variable sets
2012-11-04, by nipkow
handle non-unit clauses gracefully
2012-11-02, by blanchet
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
2012-11-02, by blanchet
use measurability prover
2012-11-02, by hoelzl
add measurability prover; add support for Borel sets
2012-11-02, by hoelzl
add syntax and a.e.-rules for (conditional) probability on predicates
2012-11-02, by hoelzl
infinite product measure is invariant under adding prefixes
2012-11-02, by hoelzl
for the product measure it is enough if only one measure is sigma-finite
2012-11-02, by hoelzl
Allow parentheses around left-hand sides of array associations
2012-11-02, by berghofe
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
2012-11-01, by blanchet
regenerated SMT certificates
2012-11-01, by blanchet
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
2012-11-01, by blanchet
fixed bool vs. prop mismatch
2012-10-31, by blanchet
removed "refute" command from Isar manual, now that it has been moved outside "Main"
2012-10-31, by blanchet
repaired "Mutabelle" after Refute move
2012-10-31, by blanchet
less verbose -- the warning will reach the users anyway by other means
2012-10-31, by blanchet
tuned messages
2012-10-31, by blanchet
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-10-31, by blanchet
fixes related to Refute's move
2012-10-31, by blanchet
added a timeout around script that relies on the network
2012-10-31, by blanchet
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
2012-10-31, by blanchet
moved Refute to "HOL/Library" to speed up building "Main" even more
2012-10-31, by blanchet
tuning
2012-10-31, by blanchet
use metaquantification when possible in Isar proofs
2012-10-31, by blanchet
tuned code
2012-10-31, by blanchet
tuning
2012-10-31, by blanchet
soft SMT timeout
2012-10-31, by blanchet
added function store_termination_rule to the signature, as it is used in Nominal2
2012-10-28, by Christian Urban
longer log, to accomodate final status line of isabelle build;
2012-10-27, by wenzelm
transfer package: error message if preprocessing goal to object-logic formula fails
2012-10-24, by huffman
transfer package: add test to prevent trying to make cterms from open terms
2012-10-24, by huffman
transfer package: more flexible handling of equality relations using is_equality predicate
2012-10-24, by huffman
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
2012-10-24, by nipkow
new theorems
2012-10-22, by kuncar
incorporated constant chars into instantiation proof for enum;
2012-10-22, by haftmann
close code theorems explicitly after preprocessing
2012-10-22, by haftmann
tuned proofs;
2012-10-22, by wenzelm
further attempts to cope with large files via option jedit_text_overview_limit;
2012-10-22, by wenzelm
more detailed Prover IDE NEWS;
2012-10-22, by wenzelm
recovered explicit error message, which was lost in b8570ea1ce25;
2012-10-21, by wenzelm
removed dead code;
2012-10-21, by wenzelm
proper signatures;
2012-10-21, by wenzelm
tuned;
2012-10-21, by wenzelm
merged
2012-10-21, by webertj
Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-19, by webertj
Tuned.
2012-10-19, by webertj
more conventional argument order;
2012-10-21, by haftmann
another refinement in the comprehension conversion
2012-10-21, by bulwahn
refined simplifier call in comprehension_conv
2012-10-21, by bulwahn
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
2012-10-21, by bulwahn
avoid STIX font, which tends to render badly;
2012-10-20, by wenzelm
extra jar for scala-2.10.0-RC1;
2012-10-20, by wenzelm
more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
2012-10-20, by wenzelm
avoid duplicate build of jars_fresh;
2012-10-20, by wenzelm
obsolete, cf. README_REPOSITORY;
2012-10-20, by wenzelm
accomodate scala-2.10.0-RC1;
2012-10-20, by wenzelm
tailored enum specification towards simple instantiation;
2012-10-20, by haftmann
refined internal structure of Enum.thy
2012-10-20, by haftmann

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

isabelle