Mon, 01 Aug 2005 19:20:25 +0200 no eq_sym_conv;
wenzelm [Mon, 01 Aug 2005 19:20:25 +0200] rev 16972
no eq_sym_conv; tuned;
Mon, 01 Aug 2005 19:20:24 +0200 removed read_cterm;
wenzelm [Mon, 01 Aug 2005 19:20:24 +0200] rev 16971
removed read_cterm; tuned;
Mon, 01 Aug 2005 19:20:23 +0200 tuned msg;
wenzelm [Mon, 01 Aug 2005 19:20:23 +0200] rev 16970
tuned msg;
Mon, 01 Aug 2005 19:20:22 +0200 PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm [Mon, 01 Aug 2005 19:20:22 +0200] rev 16969
PolyML.Compiler.printInAlphabeticalOrder := false;
Mon, 01 Aug 2005 19:20:21 +0200 polyml: use polyml-platform/version from Isabelle distribution;
wenzelm [Mon, 01 Aug 2005 19:20:21 +0200] rev 16968
polyml: use polyml-platform/version from Isabelle distribution; removed DEFS_CHAIN_HISTORY;
Mon, 01 Aug 2005 14:40:21 +0200 obsolete;
wenzelm [Mon, 01 Aug 2005 14:40:21 +0200] rev 16967
obsolete;
Mon, 01 Aug 2005 11:39:33 +0200 1. changed configuration variables for linear programming (Cplex_tools):
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
Mon, 01 Aug 2005 11:24:19 +0200 added map_filter lemmas
nipkow [Mon, 01 Aug 2005 11:24:19 +0200] rev 16965
added map_filter lemmas
Mon, 01 Aug 2005 03:27:31 +0200 Ordering is now: first by number of assumptions, second by the substitution size.
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)
Sat, 30 Jul 2005 16:50:55 +0200 addedd ID line
nipkow [Sat, 30 Jul 2005 16:50:55 +0200] rev 16963
addedd ID line
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip