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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip