| Fri, 25 Mar 2011 11:19:01 +0100 |
bulwahn |
revisiting Code_Prolog (cf. 6fe4abb9437b)
|
changeset |
files
|
| Fri, 25 Mar 2011 11:19:00 +0100 |
bulwahn |
fixed postprocessing for term presentation in quickcheck; tuned spacing
|
changeset |
files
|
| Thu, 24 Mar 2011 22:12:38 +0100 |
krauss |
enable Z3 in the test configuration
|
changeset |
files
|
| Thu, 24 Mar 2011 17:56:59 +0100 |
blanchet |
add "-?" to "nitrox" tool
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
clean up new Skolemizer code -- some old hacks are no longer necessary
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
specify proper defaults for Nitpick and Refute on TPTP + tuning
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
added "nitrox" tool (Nitpick for first-order TPTP problems) to components
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
made one more Metis example use the new Skolemizer
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
Metis examples use the new Skolemizer to test it
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
new version of Metis 2.3 (29 Dec. 2010)
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
remove newly added wrong logic
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more precise failure reporting in Sledgehammer/SMT
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
avoid evil "export_without_context", which breaks if there are local "fixes"
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
changeset |
files
|
| Thu, 24 Mar 2011 17:10:23 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 24 Mar 2011 17:10:13 +0100 |
haftmann |
added subsection on Scala specialities
|
changeset |
files
|
| Thu, 24 Mar 2011 16:39:37 +0100 |
krauss |
added more judgement day provers
|
changeset |
files
|
| Thu, 24 Mar 2011 15:29:31 +0100 |
bulwahn |
allowing special set comprehensions in values command; adding an example for special set comprehension in values
|
changeset |
files
|
| Thu, 24 Mar 2011 10:39:47 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:42 +0100 |
bulwahn |
adding documentation about the eval option in quickcheck
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:40 +0100 |
bulwahn |
adapting Quickcheck_Prolog to latest changes
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:39 +0100 |
bulwahn |
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:32 +0100 |
bulwahn |
adapting mutabelle; exporting more Quickcheck functions
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:31 +0100 |
bulwahn |
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:29 +0100 |
bulwahn |
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
|
changeset |
files
|
| Sat, 26 Mar 2011 12:01:40 +0100 |
wenzelm |
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
|
changeset |
files
|
| Sat, 26 Mar 2011 10:52:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 26 Mar 2011 10:25:17 +0100 |
wenzelm |
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
|
changeset |
files
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
changeset |
files
|
| Thu, 24 Mar 2011 16:47:24 +0100 |
wenzelm |
more direct loose_bvar1;
|
changeset |
files
|
| Thu, 24 Mar 2011 13:54:39 +0100 |
wenzelm |
indentation;
|
changeset |
files
|
| Thu, 24 Mar 2011 11:45:39 +0100 |
wenzelm |
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
|
changeset |
files
|
| Wed, 23 Mar 2011 21:07:05 +0100 |
wenzelm |
added editor mode line;
|
changeset |
files
|
| Wed, 23 Mar 2011 20:57:37 +0100 |
wenzelm |
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
|
changeset |
files
|
| Wed, 23 Mar 2011 20:51:36 +0100 |
wenzelm |
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
|
changeset |
files
|
| Wed, 23 Mar 2011 16:42:09 +0100 |
boehmes |
updated contributed components
|
changeset |
files
|
| Wed, 23 Mar 2011 15:33:17 +0100 |
boehmes |
Z3 non-commercial usage may explicitly be declined
|
changeset |
files
|
| Wed, 23 Mar 2011 14:29:29 +0100 |
boehmes |
export status function to query whether Z3 has been activated for usage within Isabelle
|
changeset |
files
|
| Wed, 23 Mar 2011 10:38:50 +0100 |
blanchet |
merge
|
changeset |
files
|
| Wed, 23 Mar 2011 10:18:42 +0100 |
blanchet |
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
|
changeset |
files
|
| Wed, 23 Mar 2011 10:06:27 +0100 |
blanchet |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
changeset |
files
|
| Wed, 23 Mar 2011 10:21:29 +0100 |
boehmes |
really be quiet
|
changeset |
files
|
| Wed, 23 Mar 2011 09:15:49 +0100 |
krauss |
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
|
changeset |
files
|
| Tue, 22 Mar 2011 21:22:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 22 Mar 2011 20:06:10 +0100 |
hoelzl |
standardized headers
|
changeset |
files
|
| Tue, 22 Mar 2011 18:53:05 +0100 |
hoelzl |
generalized Caratheodory from algebra to ring_of_sets
|
changeset |
files
|
| Tue, 22 Mar 2011 16:44:57 +0100 |
hoelzl |
add ring_of_sets and subset_class as basis for algebra
|
changeset |
files
|
| Tue, 22 Mar 2011 19:04:32 +0100 |
blanchet |
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
|
changeset |
files
|
| Tue, 22 Mar 2011 18:38:29 +0100 |
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
|
changeset |
files
|
| Tue, 22 Mar 2011 18:27:47 +0100 |
blanchet |
remove lie from documentation
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:54 +0100 |
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
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:53 +0100 |
blanchet |
make Minimizer honor "verbose" and "debug" options better
|
changeset |
files
|
| Tue, 22 Mar 2011 12:49:07 +0100 |
nipkow |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
changeset |
files
|
| Mon, 21 Mar 2011 21:10:29 +0100 |
krauss |
moved some configurations to AFP, and fixed others
|
changeset |
files
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
changeset |
files
|
| Tue, 22 Mar 2011 18:03:28 +0100 |
wenzelm |
enable inner syntax source positions by default (controlled via configuration option);
|
changeset |
files
|
| Tue, 22 Mar 2011 17:51:15 +0100 |
wenzelm |
binder_tr: more informative exception;
|
changeset |
files
|
| Tue, 22 Mar 2011 16:39:34 +0100 |
wenzelm |
Hoare syntax: strip positions where they crash translation functions;
|
changeset |
files
|
| Tue, 22 Mar 2011 16:15:50 +0100 |
wenzelm |
update_name_tr: more precise handling of explicit constraints, including positions;
|
changeset |
files
|
| Tue, 22 Mar 2011 15:32:47 +0100 |
wenzelm |
statespace syntax: strip positions -- type constraints are unexpected here;
|
changeset |
files
|
| Tue, 22 Mar 2011 14:45:48 +0100 |
wenzelm |
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
|
changeset |
files
|
| Tue, 22 Mar 2011 14:22:40 +0100 |
wenzelm |
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
|
changeset |
files
|
| Tue, 22 Mar 2011 13:55:39 +0100 |
wenzelm |
tuned indendation and parentheses;
|
changeset |
files
|
| Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
changeset |
files
|
| Tue, 22 Mar 2011 11:14:33 +0100 |
wenzelm |
pretty_string: proper handling of negative max_len;
|
changeset |
files
|
| Mon, 21 Mar 2011 23:38:32 +0100 |
wenzelm |
added Lexicon.encode_position, Lexicon.decode_position;
|
changeset |
files
|
| Mon, 21 Mar 2011 21:16:39 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 21:05:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 20:56:44 +0100 |
wenzelm |
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
|
changeset |
files
|
| Mon, 21 Mar 2011 20:15:03 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 17:14:52 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 21 Mar 2011 16:24:52 +0100 |
krauss |
added judgement day configurations
|
changeset |
files
|
| Mon, 21 Mar 2011 16:38:28 +0100 |
wenzelm |
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
|
changeset |
files
|
| Mon, 21 Mar 2011 14:46:59 +0100 |
krauss |
fixed perl error
|
changeset |
files
|
| Mon, 21 Mar 2011 14:37:10 +0100 |
krauss |
eliminated unnecessary generated ROOT.ML
|
changeset |
files
|
| Mon, 21 Mar 2011 14:25:59 +0100 |
krauss |
more precise dependencies
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:26 +0100 |
krauss |
small test case for main mirabelle functionality, which easily breaks without noticing
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:25 +0100 |
krauss |
propagate mirabelle failures properly;
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:23 +0100 |
krauss |
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
|
changeset |
files
|
| Mon, 21 Mar 2011 08:29:16 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting predicate_compile_quickcheck; tuned
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting mutabelle
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting SML_Quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
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
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending the test data generators to take the evaluation terms as arguments
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding option of evaluating terms after invocation in quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding eval option to quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding a simple datatype for representing functions in Quickcheck_Narrowing
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending code_int type more; adding narrowing instance for type int; added test case for int instance
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding size as static argument in quickcheck_narrowing compilation
|
changeset |
files
|
| Sun, 20 Mar 2011 23:07:06 +0100 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:48:08 +0100 |
wenzelm |
dropped unused structure aliases;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:47:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:26:43 +0100 |
wenzelm |
NEWS: structure Timing provides various operations for timing;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:08:12 +0100 |
wenzelm |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
changeset |
files
|
| Sun, 20 Mar 2011 21:44:38 +0100 |
wenzelm |
pure Timing.timing, without any exception handling;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:20:07 +0100 |
wenzelm |
pervasive cond_timeit;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:20:41 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:05:43 +0100 |
wenzelm |
parallel preparation of document variants, within separate directories;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:47:26 +0100 |
wenzelm |
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:34:18 +0100 |
wenzelm |
eliminated redundant doc_prefix1;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:10:09 +0100 |
wenzelm |
renamed doc_prefix2 to dump_prefix;
|
changeset |
files
|
| Sun, 20 Mar 2011 18:56:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Mar 2011 18:09:32 +0100 |
wenzelm |
tuned terminology for document variants;
|
changeset |
files
|
| Sun, 20 Mar 2011 17:40:45 +0100 |
wenzelm |
replaced File.check by specific File.check_file, File.check_dir;
|
changeset |
files
|
| Sun, 20 Mar 2011 13:49:21 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 19 Mar 2011 14:03:13 +0100 |
blanchet |
preencode value of "need" selectors in Kodkod bounds as an optimization
|
changeset |
files
|
| Sat, 19 Mar 2011 11:22:23 +0100 |
blanchet |
ignore "need" axioms for "nat"-like types
|
changeset |
files
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
changeset |
files
|
| Fri, 18 Mar 2011 17:27:28 +0100 |
blanchet |
optimize Kodkod axioms further w.r.t. "need" option
|
changeset |
files
|
| Fri, 18 Mar 2011 12:20:32 +0100 |
blanchet |
optimize Kodkod bounds of nat-like datatypes
|
changeset |
files
|
| Fri, 18 Mar 2011 12:05:23 +0100 |
blanchet |
more optimizations of bounds for "need"
|
changeset |
files
|
| Fri, 18 Mar 2011 11:43:28 +0100 |
blanchet |
optimize Kodkod bounds when "need" is specified
|
changeset |
files
|
| Fri, 18 Mar 2011 10:17:37 +0100 |
blanchet |
always destroy constructor patterns, since this seems to be always useful
|
changeset |
files
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
changeset |
files
|
| Thu, 17 Mar 2011 14:43:53 +0100 |
blanchet |
reword Nitpick's wording concerning potential counterexamples
|
changeset |
files
|