obua [Mon, 01 Aug 2005 11:39:33 +0200] rev 16966
1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML
nipkow [Mon, 01 Aug 2005 11:24:19 +0200] rev 16965
added map_filter lemmas
kleing [Mon, 01 Aug 2005 03:27:31 +0200] rev 16964
Ordering is now: first by number of assumptions, second by the substitution size.
Treat elim/dest rules like erule/drule would:
* "elim" is now a subset of "dest" and matches on conclusion of goal and
major premise against any premise of goal. Computed substitution size
takes both into account.
* "dest" no longer has a restriction that limits its conclusion to a var.
(contributed by Raf)
nipkow [Sat, 30 Jul 2005 16:50:55 +0200] rev 16963
addedd ID line
avigad [Fri, 29 Jul 2005 19:47:41 +0200] rev 16962
mentioned Ln in NEWS
avigad [Fri, 29 Jul 2005 19:47:34 +0200] rev 16961
fixed minor typo in comments
avigad [Fri, 29 Jul 2005 19:47:27 +0200] rev 16960
changed import to Ln
avigad [Fri, 29 Jul 2005 19:47:19 +0200] rev 16959
added a new theory; properties of ln
wenzelm [Fri, 29 Jul 2005 16:16:44 +0200] rev 16958
P.opt_locale_target;
paulson [Fri, 29 Jul 2005 15:20:29 +0200] rev 16957
nameless theorems: better names, flag to omit them