avigad [Wed, 03 Aug 2005 14:48:30 +0200] rev 17011
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
avigad [Wed, 03 Aug 2005 14:48:22 +0200] rev 17010
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad [Wed, 03 Aug 2005 14:48:13 +0200] rev 17009
import FixedPoint instead of Gfp
avigad [Wed, 03 Aug 2005 14:48:07 +0200] rev 17008
removed Gfp
avigad [Wed, 03 Aug 2005 14:47:57 +0200] rev 17007
removed Lfp
avigad [Wed, 03 Aug 2005 14:47:51 +0200] rev 17006
combined Lfp and Gfp to FixedPoint
wenzelm [Tue, 02 Aug 2005 21:29:06 +0200] rev 17005
tuned ML_OPTIONS;
wenzelm [Tue, 02 Aug 2005 19:47:14 +0200] rev 17004
export clear_ss;
wenzelm [Tue, 02 Aug 2005 19:47:13 +0200] rev 17003
added unfold_tac (Simplifier.inherit_bounds);
wenzelm [Tue, 02 Aug 2005 19:47:12 +0200] rev 17002
simprocs: Simplifier.inherit_bounds;
wenzelm [Tue, 02 Aug 2005 19:47:11 +0200] rev 17001
tuned;
ballarin [Tue, 02 Aug 2005 16:52:21 +0200] rev 17000
First version of interpretation in locales. Not yet fully functional.
ballarin [Tue, 02 Aug 2005 16:50:55 +0200] rev 16999
Turned simp_implies into binary operator.
nipkow [Tue, 02 Aug 2005 13:13:18 +0200] rev 16998
Added filter lemma
wenzelm [Mon, 01 Aug 2005 19:21:38 +0200] rev 16997
* Pure/Simplifier: improved handling of bound variables;
wenzelm [Mon, 01 Aug 2005 19:20:49 +0200] rev 16996
determine Poly/ML runtime system version
wenzelm [Mon, 01 Aug 2005 19:20:48 +0200] rev 16995
obsolete;
wenzelm [Mon, 01 Aug 2005 19:20:48 +0200] rev 16994
determine Poly/ML's idea of current hardware and operating system type;
wenzelm [Mon, 01 Aug 2005 19:20:47 +0200] rev 16993
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:46 +0200] rev 16992
Thm.full_prop_of;
wenzelm [Mon, 01 Aug 2005 19:20:45 +0200] rev 16991
Compress.term;
wenzelm [Mon, 01 Aug 2005 19:20:44 +0200] rev 16990
removed atless (use term_ord instead);
removed (inefficient) insert_aterm;
improved bound: nameless, avoid allocating new strings;
tuned sort_ord/typ_ord: dict_ord;
tuned abstract_over: SAME;
tuned add_term_vars/frees: OrdList.insert;
removed compress_type/compress_type (cf. compress.ML);
wenzelm [Mon, 01 Aug 2005 19:20:43 +0200] rev 16989
export MataSimplifier.inherit_bounds;
wenzelm [Mon, 01 Aug 2005 19:20:42 +0200] rev 16988
Compress.typ;
wenzelm [Mon, 01 Aug 2005 19:20:41 +0200] rev 16987
Compress.init_data;
wenzelm [Mon, 01 Aug 2005 19:20:40 +0200] rev 16986
nameless Term.bound;
wenzelm [Mon, 01 Aug 2005 19:20:39 +0200] rev 16985
improved bounds: nameless Term.bound, recover names for output;
wenzelm [Mon, 01 Aug 2005 19:20:38 +0200] rev 16984
tuned dict_ord;
wenzelm [Mon, 01 Aug 2005 19:20:37 +0200] rev 16983
replaced atless by term_ord;
wenzelm [Mon, 01 Aug 2005 19:20:36 +0200] rev 16982
chain_history: turned into runtime flag;
added monomorphic;
removed (inefficient) fast_overloading_info;
Compress.typ;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:35 +0200] rev 16981
compression of terms and types by sharing common subtrees;
wenzelm [Mon, 01 Aug 2005 19:20:34 +0200] rev 16980
added compress.ML;
wenzelm [Mon, 01 Aug 2005 19:20:33 +0200] rev 16979
Term.is_bound;
wenzelm [Mon, 01 Aug 2005 19:20:32 +0200] rev 16978
tuned signature;
wenzelm [Mon, 01 Aug 2005 19:20:31 +0200] rev 16977
no eq_commute;
wenzelm [Mon, 01 Aug 2005 19:20:30 +0200] rev 16976
Defs.monomorphic;
wenzelm [Mon, 01 Aug 2005 19:20:29 +0200] rev 16975
Sign.read_term;
wenzelm [Mon, 01 Aug 2005 19:20:28 +0200] rev 16974
more zcong_sym;
wenzelm [Mon, 01 Aug 2005 19:20:26 +0200] rev 16973
simprocs: Simplifier.inherit_bounds;
wenzelm [Mon, 01 Aug 2005 19:20:25 +0200] rev 16972
no eq_sym_conv;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:24 +0200] rev 16971
removed read_cterm;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:23 +0200] rev 16970
tuned msg;
wenzelm [Mon, 01 Aug 2005 19:20:22 +0200] rev 16969
PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm [Mon, 01 Aug 2005 19:20:21 +0200] rev 16968
polyml: use polyml-platform/version from Isabelle distribution;
removed DEFS_CHAIN_HISTORY;
wenzelm [Mon, 01 Aug 2005 14:40:21 +0200] rev 16967
obsolete;
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
paulson [Thu, 28 Jul 2005 17:56:27 +0200] rev 16956
invents theorem names; also patches write_out_clasimp
paulson [Thu, 28 Jul 2005 17:55:39 +0200] rev 16955
dead code
paulson [Thu, 28 Jul 2005 17:54:39 +0200] rev 16954
new function trim_ends
paulson [Thu, 28 Jul 2005 17:54:22 +0200] rev 16953
uniform treatment of variable prefixes
haftmann [Thu, 28 Jul 2005 16:59:30 +0200] rev 16952
corrected some typos