Sat, 14 Apr 2012 23:52:17 +0100 Mirabelle now gives usage info when no arguments given
sultana [Sat, 14 Apr 2012 23:52:17 +0100] rev 47479
Mirabelle now gives usage info when no arguments given
Sat, 14 Apr 2012 23:52:17 +0100 switched from using sed to perl in mirabelle tool
sultana [Sat, 14 Apr 2012 23:52:17 +0100] rev 47478
switched from using sed to perl in mirabelle tool
Sat, 14 Apr 2012 23:52:17 +0100 renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
sultana [Sat, 14 Apr 2012 23:52:17 +0100] rev 47477
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
Sat, 14 Apr 2012 23:34:18 +0200 refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm [Sat, 14 Apr 2012 23:34:18 +0200] rev 47476
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"; clarified thin_prems_tac: fail as tactic without error;
Sat, 14 Apr 2012 20:44:53 +0200 merged;
wenzelm [Sat, 14 Apr 2012 20:44:53 +0200] rev 47475
merged;
Sat, 14 Apr 2012 19:29:31 +0200 removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
krauss [Sat, 14 Apr 2012 19:29:31 +0200] rev 47474
removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
Sat, 14 Apr 2012 15:08:59 +0100 aligned tptp_graph dependencies to Isabelle conventions;
sultana [Sat, 14 Apr 2012 15:08:59 +0100] rev 47473
aligned tptp_graph dependencies to Isabelle conventions;
Sat, 14 Apr 2012 20:10:10 +0200 more ambitious isatest settings using polyml-svn (e.g. 1487);
wenzelm [Sat, 14 Apr 2012 20:10:10 +0200] rev 47472
more ambitious isatest settings using polyml-svn (e.g. 1487);
Sat, 14 Apr 2012 19:09:34 +0200 use official TextArea.isCaretVisible and thus follow the "blink" flag;
wenzelm [Sat, 14 Apr 2012 19:09:34 +0200] rev 47471
use official TextArea.isCaretVisible and thus follow the "blink" flag; updated jedit_build component;
Sat, 14 Apr 2012 18:28:11 +0200 display more memory;
wenzelm [Sat, 14 Apr 2012 18:28:11 +0200] rev 47470
display more memory;
Sat, 14 Apr 2012 17:26:08 +0200 keyword ";" is declared via prover (as "minor", not "diag");
wenzelm [Sat, 14 Apr 2012 17:26:08 +0200] rev 47469
keyword ";" is declared via prover (as "minor", not "diag");
Sat, 14 Apr 2012 17:15:57 +0200 outermost SELECT_GOAL potentially improves performance;
wenzelm [Sat, 14 Apr 2012 17:15:57 +0200] rev 47468
outermost SELECT_GOAL potentially improves performance;
(0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 +10000 +30000 tip