Tue, 22 Mar 2011 16:44:57 +0100add ring_of_sets and subset_class as basis for algebra
hoelzl [Tue, 22 Mar 2011 16:44:57 +0100] rev 42920
add ring_of_sets and subset_class as basis for algebra

Tue, 22 Mar 2011 19:04:32 +0100added 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 42919
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 +0100added "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 42918
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 +0100remove lie from documentation
blanchet [Tue, 22 Mar 2011 18:27:47 +0100] rev 42917
remove lie from documentation

Tue, 22 Mar 2011 17:20:54 +0100let 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 42916
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 +0100make Minimizer honor "verbose" and "debug" options better
blanchet [Tue, 22 Mar 2011 17:20:53 +0100] rev 42915
make Minimizer honor "verbose" and "debug" options better

Tue, 22 Mar 2011 12:49:07 +0100fixed 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 42914
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples

Mon, 21 Mar 2011 21:10:29 +0100moved some configurations to AFP, and fixed others
krauss [Mon, 21 Mar 2011 21:10:29 +0100] rev 42913
moved some configurations to AFP, and fixed others

Mon, 21 Mar 2011 17:14:52 +0100merged
wenzelm [Mon, 21 Mar 2011 17:14:52 +0100] rev 42912
merged

Mon, 21 Mar 2011 16:38:28 +0100another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
wenzelm [Mon, 21 Mar 2011 16:38:28 +0100] rev 42911
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);