Wed, 23 Mar 2011 15:33:17 +0100 Z3 non-commercial usage may explicitly be declined
boehmes [Wed, 23 Mar 2011 15:33:17 +0100] rev 42075
Z3 non-commercial usage may explicitly be declined
Wed, 23 Mar 2011 14:29:29 +0100 export status function to query whether Z3 has been activated for usage within Isabelle
boehmes [Wed, 23 Mar 2011 14:29:29 +0100] rev 42074
export status function to query whether Z3 has been activated for usage within Isabelle
Wed, 23 Mar 2011 10:38:50 +0100 merge
blanchet [Wed, 23 Mar 2011 10:38:50 +0100] rev 42073
merge
Wed, 23 Mar 2011 10:18:42 +0100 avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet [Wed, 23 Mar 2011 10:18:42 +0100] rev 42072
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
Wed, 23 Mar 2011 10:06:27 +0100 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet [Wed, 23 Mar 2011 10:06:27 +0100] rev 42071
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle
Wed, 23 Mar 2011 10:21:29 +0100 really be quiet
boehmes [Wed, 23 Mar 2011 10:21:29 +0100] rev 42070
really be quiet
Wed, 23 Mar 2011 09:15:49 +0100 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
krauss [Wed, 23 Mar 2011 09:15:49 +0100] rev 42069
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
Tue, 22 Mar 2011 21:22:50 +0100 merged
wenzelm [Tue, 22 Mar 2011 21:22:50 +0100] rev 42068
merged
Tue, 22 Mar 2011 20:06:10 +0100 standardized headers
hoelzl [Tue, 22 Mar 2011 20:06:10 +0100] rev 42067
standardized headers
Tue, 22 Mar 2011 18:53:05 +0100 generalized Caratheodory from algebra to ring_of_sets
hoelzl [Tue, 22 Mar 2011 18:53:05 +0100] rev 42066
generalized Caratheodory from algebra to ring_of_sets
Tue, 22 Mar 2011 16:44:57 +0100 add ring_of_sets and subset_class as basis for algebra
hoelzl [Tue, 22 Mar 2011 16:44:57 +0100] rev 42065
add ring_of_sets and subset_class as basis for algebra
Tue, 22 Mar 2011 19:04:32 +0100 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
blanchet [Tue, 22 Mar 2011 19:04:32 +0100] rev 42064
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
Tue, 22 Mar 2011 18:38:29 +0100 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
blanchet [Tue, 22 Mar 2011 18:38:29 +0100] rev 42063
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
Tue, 22 Mar 2011 18:27:47 +0100 remove lie from documentation
blanchet [Tue, 22 Mar 2011 18:27:47 +0100] rev 42062
remove lie from documentation
Tue, 22 Mar 2011 17:20:54 +0100 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
blanchet [Tue, 22 Mar 2011 17:20:54 +0100] rev 42061
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
Tue, 22 Mar 2011 17:20:53 +0100 make Minimizer honor "verbose" and "debug" options better
blanchet [Tue, 22 Mar 2011 17:20:53 +0100] rev 42060
make Minimizer honor "verbose" and "debug" options better
Tue, 22 Mar 2011 12:49:07 +0100 fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
nipkow [Tue, 22 Mar 2011 12:49:07 +0100] rev 42059
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
Mon, 21 Mar 2011 21:10:29 +0100 moved some configurations to AFP, and fixed others
krauss [Mon, 21 Mar 2011 21:10:29 +0100] rev 42058
moved some configurations to AFP, and fixed others
Tue, 22 Mar 2011 20:44:47 +0100 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm [Tue, 22 Mar 2011 20:44:47 +0100] rev 42057
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
Tue, 22 Mar 2011 18:03:28 +0100 enable inner syntax source positions by default (controlled via configuration option);
wenzelm [Tue, 22 Mar 2011 18:03:28 +0100] rev 42056
enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;
Tue, 22 Mar 2011 17:51:15 +0100 binder_tr: more informative exception;
wenzelm [Tue, 22 Mar 2011 17:51:15 +0100] rev 42055
binder_tr: more informative exception;
Tue, 22 Mar 2011 16:39:34 +0100 Hoare syntax: strip positions where they crash translation functions;
wenzelm [Tue, 22 Mar 2011 16:39:34 +0100] rev 42054
Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!);
Tue, 22 Mar 2011 16:15:50 +0100 update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm [Tue, 22 Mar 2011 16:15:50 +0100] rev 42053
update_name_tr: more precise handling of explicit constraints, including positions;
Tue, 22 Mar 2011 15:32:47 +0100 statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm [Tue, 22 Mar 2011 15:32:47 +0100] rev 42052
statespace syntax: strip positions -- type constraints are unexpected here;
Tue, 22 Mar 2011 14:45:48 +0100 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm [Tue, 22 Mar 2011 14:45:48 +0100] rev 42051
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
Tue, 22 Mar 2011 14:22:40 +0100 datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm [Tue, 22 Mar 2011 14:22:40 +0100] rev 42050
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
Tue, 22 Mar 2011 13:55:39 +0100 tuned indendation and parentheses;
wenzelm [Tue, 22 Mar 2011 13:55:39 +0100] rev 42049
tuned indendation and parentheses;
Tue, 22 Mar 2011 13:32:20 +0100 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm [Tue, 22 Mar 2011 13:32:20 +0100] rev 42048
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
Tue, 22 Mar 2011 11:14:33 +0100 pretty_string: proper handling of negative max_len;
wenzelm [Tue, 22 Mar 2011 11:14:33 +0100] rev 42047
pretty_string: proper handling of negative max_len;
Mon, 21 Mar 2011 23:38:32 +0100 added Lexicon.encode_position, Lexicon.decode_position;
wenzelm [Mon, 21 Mar 2011 23:38:32 +0100] rev 42046
added Lexicon.encode_position, Lexicon.decode_position;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip