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