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

enable Z3 in the test configuration
2011-03-24, by krauss
add "-?" to "nitrox" tool
2011-03-24, by blanchet
clean up new Skolemizer code -- some old hacks are no longer necessary
2011-03-24, by blanchet
specify proper defaults for Nitpick and Refute on TPTP + tuning
2011-03-24, by blanchet
added "nitrox" tool (Nitpick for first-order TPTP problems) to components
2011-03-24, by blanchet
made one more Metis example use the new Skolemizer
2011-03-24, by blanchet
Metis examples use the new Skolemizer to test it
2011-03-24, by blanchet
new version of Metis 2.3 (29 Dec. 2010)
2011-03-24, by blanchet
remove newly added wrong logic
2011-03-24, by blanchet
more precise failure reporting in Sledgehammer/SMT
2011-03-24, by blanchet
avoid evil "export_without_context", which breaks if there are local "fixes"
2011-03-24, by blanchet
more robust handling of variables in new Skolemizer
2011-03-24, by blanchet
merged
2011-03-24, by haftmann
added subsection on Scala specialities
2011-03-24, by haftmann
added more judgement day provers
2011-03-24, by krauss
allowing special set comprehensions in values command; adding an example for special set comprehension in values
2011-03-24, by bulwahn
merged
2011-03-24, by bulwahn
adding documentation about the eval option in quickcheck
2011-03-23, by bulwahn
adapting Quickcheck_Prolog to latest changes
2011-03-23, by bulwahn
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
2011-03-23, by bulwahn
adapting mutabelle; exporting more Quickcheck functions
2011-03-23, by bulwahn
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
2011-03-23, by bulwahn
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
2011-03-23, by bulwahn
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
2011-03-26, by wenzelm
tuned;
2011-03-26, by wenzelm
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
2011-03-26, by wenzelm
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-03-24, by wenzelm
more direct loose_bvar1;
2011-03-24, by wenzelm
indentation;
2011-03-24, by wenzelm
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
2011-03-24, by wenzelm
added editor mode line;
2011-03-23, by wenzelm
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
2011-03-23, by wenzelm
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
2011-03-23, by wenzelm
updated contributed components
2011-03-23, by boehmes
Z3 non-commercial usage may explicitly be declined
2011-03-23, by boehmes
export status function to query whether Z3 has been activated for usage within Isabelle
2011-03-23, by boehmes
merge
2011-03-23, by blanchet
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
2011-03-23, by blanchet
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
2011-03-23, by blanchet
really be quiet
2011-03-23, by boehmes
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
2011-03-23, by krauss
merged
2011-03-22, by wenzelm
standardized headers
2011-03-22, by hoelzl
generalized Caratheodory from algebra to ring_of_sets
2011-03-22, by hoelzl
add ring_of_sets and subset_class as basis for algebra
2011-03-22, by hoelzl
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
2011-03-22, by blanchet
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
2011-03-22, by blanchet
remove lie from documentation
2011-03-22, by blanchet
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
2011-03-22, by blanchet
make Minimizer honor "verbose" and "debug" options better
2011-03-22, by blanchet
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
2011-03-22, by nipkow
moved some configurations to AFP, and fixed others
2011-03-21, by krauss
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22, by wenzelm
enable inner syntax source positions by default (controlled via configuration option);
2011-03-22, by wenzelm
binder_tr: more informative exception;
2011-03-22, by wenzelm
Hoare syntax: strip positions where they crash translation functions;
2011-03-22, by wenzelm
update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22, by wenzelm
statespace syntax: strip positions -- type constraints are unexpected here;
2011-03-22, by wenzelm
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
2011-03-22, by wenzelm
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
2011-03-22, by wenzelm

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

isabelle