isabelle: Graph

adhoc token style for free/bound;
2011-03-27, by wenzelm
decode_term/disambig: report resolved term variables for the unique (!) result;
2011-03-27, by wenzelm
removed unclear comments stemming from ed24ba6f69aa;
2011-03-27, by wenzelm
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
2011-03-26, by wenzelm
added Future.cond_forks convenience;
2011-03-26, by wenzelm
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
2011-03-26, by wenzelm
tuned;
2011-03-26, by wenzelm
more direct loose_bvar1;
2011-03-26, by wenzelm
suppress Mercurial backup files;
2011-03-26, by wenzelm
updated generated file;
2011-03-26, by wenzelm
merged
2011-03-26, by wenzelm
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
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
tuned indendation and parentheses;
2011-03-22, by wenzelm
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
2011-03-22, by wenzelm
pretty_string: proper handling of negative max_len;
2011-03-22, by wenzelm
added Lexicon.encode_position, Lexicon.decode_position;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
merged
2011-03-21, by wenzelm
added judgement day configurations
2011-03-21, by krauss
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
2011-03-21, by wenzelm
fixed perl error
2011-03-21, by krauss
eliminated unnecessary generated ROOT.ML
2011-03-21, by krauss
more precise dependencies
2011-03-21, by krauss
small test case for main mirabelle functionality, which easily breaks without noticing
2011-03-21, by krauss
propagate mirabelle failures properly;
2011-03-21, by krauss
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
2011-03-21, by krauss
merged
2011-03-21, by bulwahn
adapting predicate_compile_quickcheck; tuned
2011-03-18, by bulwahn
adapting mutabelle
2011-03-18, by bulwahn
adapting SML_Quickcheck
2011-03-18, by bulwahn
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
2011-03-18, by bulwahn
extending the test data generators to take the evaluation terms as arguments
2011-03-18, by bulwahn
adding option of evaluating terms after invocation in quickcheck
2011-03-18, by bulwahn
adding eval option to quickcheck
2011-03-18, by bulwahn
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
2011-03-18, by bulwahn
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
2011-03-18, by bulwahn
adding a simple datatype for representing functions in Quickcheck_Narrowing
2011-03-18, by bulwahn
extending code_int type more; adding narrowing instance for type int; added test case for int instance
2011-03-18, by bulwahn
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
2011-03-18, by bulwahn
adding size as static argument in quickcheck_narrowing compilation
2011-03-18, by bulwahn
modernized specifications;
2011-03-20, by wenzelm
dropped unused structure aliases;
2011-03-20, by wenzelm
tuned;
2011-03-20, by wenzelm
NEWS: structure Timing provides various operations for timing;
2011-03-20, by wenzelm
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
2011-03-20, by wenzelm
pure Timing.timing, without any exception handling;
2011-03-20, by wenzelm