| 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
|