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 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

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

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

isabelle