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

refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
2010-11-17, by wenzelm
less parentheses, cf. Session.welcome;
2010-11-17, by wenzelm
avoid spam;
2010-11-16, by wenzelm
more robust determination of java executable;
2010-11-16, by wenzelm
init_component: require absolute path (when invoked by user scripts);
2010-11-16, by wenzelm
more explicit explanation of init_component shell function;
2010-11-16, by wenzelm
paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
2010-11-16, by wenzelm
tuned message;
2010-11-16, by wenzelm
post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
2010-11-16, by wenzelm
more reasonably defaults for typical laptops (2 GB RAM, 2 cores);
2010-11-16, by wenzelm
added forall2 predicate lifter
2010-11-16, by haftmann
merged
2010-11-15, by wenzelm
merged
2010-11-15, by boehmes
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15, by boehmes
honour timeouts which are not rounded to full seconds
2010-11-15, by boehmes
better error message
2010-11-15, by blanchet
better error message
2010-11-15, by blanchet
merged
2010-11-15, by wenzelm
cosmetics
2010-11-15, by blanchet
interpret SMT_Failure.Solver_Crashed correctly
2010-11-15, by blanchet
turn on Sledgehammer verbosity so we can track down crashes
2010-11-15, by blanchet
pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-15, by blanchet
merged
2010-11-15, by boehmes
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
2010-11-15, by boehmes
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
2010-11-15, by boehmes
merged
2010-11-15, by bulwahn
ignoring the constant STR in the predicate compiler
2010-11-15, by bulwahn
non-executable source files;
2010-11-15, by wenzelm
eliminated old-style sed in favour of builtin regex matching;
2010-11-15, by wenzelm
more robust treatment of spaces in file names;
2010-11-15, by wenzelm
tuned error messages;
2010-11-15, by wenzelm
merged
2010-11-15, by wenzelm
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
re-generalized type of prod_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
formal dependency on b2i files
2010-11-15, by boehmes
merged
2010-11-14, by boehmes
check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12, by boehmes
updated README;
2010-11-14, by wenzelm
tuned;
2010-11-14, by wenzelm
cover 'write' as primitive proof command;
2010-11-14, by wenzelm
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-14, by wenzelm
somewhat adhoc replacement for 'thus' and 'hence';
2010-11-13, by wenzelm
always print state of proof commands (notably "qed" etc.);
2010-11-13, by wenzelm
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13, by wenzelm
tuned message;
2010-11-13, by wenzelm
proper escape in regex;
2010-11-13, by wenzelm
report malformed symbols;
2010-11-13, by wenzelm
qualified Symbol_Pos.symbol;
2010-11-13, by wenzelm
total Symbol.source;
2010-11-13, by wenzelm
eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13, by wenzelm
treat Unicode "replacement character" (i.e. decoding error) is malformed;
2010-11-13, by wenzelm
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-11-13, by wenzelm
tuned;
2010-11-13, by wenzelm
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-13, by wenzelm
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
2010-11-13, by wenzelm
updated README;
2010-11-13, by wenzelm
defensive defaults for more robust experience for new users;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
preliminary support for newer versions of Z3
2010-11-12, by boehmes
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-12, by boehmes

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

isabelle