Wed, 23 Mar 2011 15:33:17 +0100 boehmes Z3 non-commercial usage may explicitly be declined
Wed, 23 Mar 2011 14:29:29 +0100 boehmes export status function to query whether Z3 has been activated for usage within Isabelle
Wed, 23 Mar 2011 10:38:50 +0100 blanchet merge
Wed, 23 Mar 2011 10:18:42 +0100 blanchet avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
Wed, 23 Mar 2011 10:06:27 +0100 blanchet move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
Wed, 23 Mar 2011 10:21:29 +0100 boehmes really be quiet
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
Tue, 22 Mar 2011 21:22:50 +0100 wenzelm merged
Tue, 22 Mar 2011 20:06:10 +0100 hoelzl standardized headers
Tue, 22 Mar 2011 18:53:05 +0100 hoelzl generalized Caratheodory from algebra to ring_of_sets
Tue, 22 Mar 2011 16:44:57 +0100 hoelzl add ring_of_sets and subset_class as basis for algebra
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
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
Tue, 22 Mar 2011 18:27:47 +0100 blanchet remove lie from documentation
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
(0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip