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

SML_makeall: run with -j 3
2011-03-26, by krauss
fixed incomplete rename (1cdf54e845fa)
2011-03-25, by krauss
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
2011-03-25, by krauss
merged
2011-03-25, by bulwahn
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
2011-03-25, by bulwahn
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
2011-03-24, by krauss
mira interface to 'isabelle make' in addition to usedir and makeall;
2011-03-24, by krauss
clarified
2011-03-24, by krauss
parameterize configurations by custom settings
2011-03-24, by krauss
Change coercion for RealDef to use function application (not composition)
2011-03-25, by noschinl
revisiting Code_Prolog (cf. 6fe4abb9437b)
2011-03-25, by bulwahn
fixed postprocessing for term presentation in quickcheck; tuned spacing
2011-03-25, by bulwahn
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

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

isabelle