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

temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
2012-05-31, by huffman
temporarily comment out nitpick examples broken by changes to Int.thy
2012-05-30, by huffman
convert Int.thy to use lifting and transfer
2012-05-30, by huffman
remove unnecessary simp rules involving Abs_Integ
2012-05-30, by huffman
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
2012-05-30, by boehmes
merged
2012-05-30, by Andreas Lochbihler
remove pretty syntax for FinFuns at the end and provide separate syntax theory
2012-05-30, by Andreas Lochbihler
add lemma set_of_image_mset
2012-05-29, by huffman
merged
2012-05-30, by Andreas Lochbihler
eliminated remaining sub- and superscripts in FinFun syntax
2012-05-30, by Andreas Lochbihler
syntax for FinFun composition without subscripts
2012-05-30, by Andreas Lochbihler
FinFun pseudo-constructor syntax without superscripts
2012-05-30, by Andreas Lochbihler
replace FinFun application syntax with $
2012-05-30, by Andreas Lochbihler
removed subscripts from FinFun type syntax
2012-05-30, by Andreas Lochbihler
improve code setup for set equality
2012-05-30, by Andreas Lochbihler
add code equation for coset xs = set ys
2012-05-29, by Andreas Lochbihler
tuned proofs
2012-05-29, by Andreas Lochbihler
use bundle in FinFun
2012-05-29, by Andreas Lochbihler
unify Rep_finfun and finfun_apply
2012-05-29, by Andreas Lochbihler
move FinFuns from AFP to repository
2012-05-29, by Andreas Lochbihler
discontinued unused unzip/untar;
2012-05-30, by wenzelm
update GUI components after init;
2012-05-29, by wenzelm
merged
2012-05-29, by wenzelm
don't be so aggressive during unfolding id and o
2012-05-29, by kuncar
reordered sections
2012-05-29, by huffman
tuned message;
2012-05-29, by wenzelm
separate syslog dockable -- discontinued tendency of sub-window management via tabs;
2012-05-29, by wenzelm
clarified prover startup: no timeout, read stderr more carefully;
2012-05-29, by wenzelm
need to close_input before expecting threads to terminate/join;
2012-05-29, by wenzelm
make double sure that GUI components are up-to-date after init;
2012-05-29, by wenzelm
tuned message;
2012-05-29, by wenzelm
more explicit treatment of return code vs. session phase;
2012-05-29, by wenzelm
tuned signature;
2012-05-29, by wenzelm
separate README dockable, which allows to make it more prominent first and remove it later;
2012-05-29, by wenzelm
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
2012-05-29, by bulwahn
shortened yet more multiset proofs;
2012-05-29, by huffman
remove unused intermediate lemma
2012-05-29, by huffman
shortened more multiset proofs
2012-05-29, by huffman
shortened some proofs
2012-05-29, by huffman
use transfer method for instance proof
2012-05-29, by huffman
tweaked remote Vampire setup
2012-05-28, by blanchet
update docs
2012-05-28, by blanchet
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
2012-05-28, by blanchet
don't generate definitions for LEO-II -- this cuases more harm than good
2012-05-28, by blanchet
dropped sort constraints on datatype specifications
2012-05-28, by haftmann
potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
2012-05-25, by wenzelm
tuned proofs;
2012-05-25, by wenzelm
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
2012-05-25, by wenzelm
ignore empty messages even on tty, e.g. relevant for Isabelle_System.bash_output err output;
2012-05-25, by wenzelm
discontinued obsolete Cygwin module;
2012-05-24, by wenzelm
eliminated unused Cygwin download;
2012-05-24, by wenzelm
simplified Cygwin root: warm start via env, cold start via property, no registry magic;
2012-05-24, by wenzelm
include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;
2012-05-24, by wenzelm
tuned proofs;
2012-05-24, by wenzelm
less warning in scala-2.10.0-M3;
2012-05-24, by wenzelm
avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0;
2012-05-24, by wenzelm
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
2012-05-24, by blanchet
fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality
2012-05-24, by blanchet
more robust Swing_Thread.now: allow body to fail;
2012-05-24, by wenzelm
tuned proofs;
2012-05-24, by wenzelm

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

isabelle