berghofe [Fri, 05 Aug 2005 19:58:30 +0200] rev 17025
Added ENTCS 2000 paper by Aleksey Nogin.
berghofe [Fri, 05 Aug 2005 19:57:57 +0200] rev 17024
New case study: pigeonhole principle.
berghofe [Fri, 05 Aug 2005 19:56:58 +0200] rev 17023
Added Extraction/Pigeonhole.
nipkow [Fri, 05 Aug 2005 12:20:30 +0200] rev 17022
added Brian Hufmann's finite instances
berghofe [Wed, 03 Aug 2005 16:43:39 +0200] rev 17021
Fixed bug in code generator for let and split leading to ill-formed code.
berghofe [Wed, 03 Aug 2005 16:28:22 +0200] rev 17020
Adapted to new argument format of MinProof constructor.
berghofe [Wed, 03 Aug 2005 16:26:16 +0200] rev 17019
Adapted to new interface og thms_of_proof / axms_of_proof.
berghofe [Wed, 03 Aug 2005 16:25:22 +0200] rev 17018
Adapted to new interface of thms_of_proof.
berghofe [Wed, 03 Aug 2005 16:24:52 +0200] rev 17017
- Tuned handling of oracles
- Put arguments of axms_of_proof and thms_of_proof into "canonical order"
avigad [Wed, 03 Aug 2005 14:49:04 +0200] rev 17016
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad [Wed, 03 Aug 2005 14:48:56 +0200] rev 17015
changes from renaming of exp_ge_add_one_self
avigad [Wed, 03 Aug 2005 14:48:50 +0200] rev 17014
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad [Wed, 03 Aug 2005 14:48:42 +0200] rev 17013
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
avigad [Wed, 03 Aug 2005 14:48:36 +0200] rev 17012
added extra transitivity rules
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