| 2008-01-25 |
wenzelm |
2008-01-25 |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
|
file | diff | annotate |
| 2007-12-14 |
wenzelm |
2007-12-14 |
added ISABELLE_LINE_EDITOR;
tuned;
|
file | diff | annotate |
| 2007-11-28 |
wenzelm |
2007-11-28 |
polyml: default heap size is back to -H 200 (people are still using
machines with < 1GB of memory; no need to workaround heap problems of
polyml-5.0 anymore);
|
file | diff | annotate |
| 2007-11-08 |
wenzelm |
2007-11-08 |
tuned comments;
|
file | diff | annotate |
| 2007-10-20 |
wenzelm |
2007-10-20 |
tuned;
|
file | diff | annotate |
| 2007-09-17 |
haftmann |
2007-09-17 |
platform-sensitive default location for ATP provers
|
file | diff | annotate |
| 2007-09-06 |
paulson |
2007-09-06 |
Auto-config of E_HOME, SPASS_HOME, VAMPIRE_HOME
|
file | diff | annotate |
| 2007-08-29 |
wenzelm |
2007-08-29 |
renamed POLYML_LINK_OPTIONS to POLY_LINK_OPTIONS;
|
file | diff | annotate |
| 2007-08-29 |
wenzelm |
2007-08-29 |
added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);
|
file | diff | annotate |
| 2007-08-27 |
wenzelm |
2007-08-27 |
HOL_USEDIR_OPTIONS: no special -M setting (now works with multithreaded);
|
file | diff | annotate |
| 2007-08-10 |
wenzelm |
2007-08-10 |
HOL_USEDIR_OPTIONS: default to -M 1 (more robust);
|
file | diff | annotate |
| 2007-08-10 |
wenzelm |
2007-08-10 |
added jEdit mode spec;
tuned comments;
|
file | diff | annotate |
| 2007-07-23 |
kleing |
2007-07-23 |
increase default max heap size for poly to -H 500 (this is what isatest uses,
-H 80 is not enough for HOL on at-mac-poly).
|
file | diff | annotate |
| 2007-07-17 |
wenzelm |
2007-07-17 |
added ISABELLE_FILE_IDENT (command line for source file identification);
|
file | diff | annotate |
| 2007-05-30 |
wenzelm |
2007-05-30 |
tuned USEDIR_OPTIONS;
PDF_VIEWER: try to be smart for MacOS (Darwin);
|
file | diff | annotate |
| 2007-01-21 |
wenzelm |
2007-01-21 |
tuned comments
|
file | diff | annotate |
| 2006-12-13 |
wenzelm |
2006-12-13 |
tuned comments;
|
file | diff | annotate |
| 2006-12-05 |
wenzelm |
2006-12-05 |
setup for polyml-5.0;
|
file | diff | annotate |
| 2006-11-23 |
wenzelm |
2006-11-23 |
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
|
file | diff | annotate |
| 2006-11-04 |
wenzelm |
2006-11-04 |
HOL_USEDIR_OPTIONS: -p 1 by default;
|
file | diff | annotate |
| 2006-10-11 |
wenzelm |
2006-10-11 |
increased heap size for polyml-4.9.1;
|
file | diff | annotate |
| 2006-09-28 |
wenzelm |
2006-09-28 |
added Poly/ML 4.9.1 (experimental!);
|
file | diff | annotate |
| 2006-07-07 |
webertj |
2006-07-07 |
added support for MiniSat 1.14
|
file | diff | annotate |
| 2006-03-21 |
wenzelm |
2006-03-21 |
fixed example;
|
file | diff | annotate |
| 2006-02-10 |
wenzelm |
2006-02-10 |
simplified polyml example;
|
file | diff | annotate |
| 2005-10-21 |
wenzelm |
2005-10-21 |
added simplified settings for Poly/ML 4.x (commented out);
|
file | diff | annotate |
| 2005-10-21 |
wenzelm |
2005-10-21 |
reverted (accidental?) change of 1.148;
|
file | diff | annotate |
| 2005-10-21 |
mengj |
2005-10-21 |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
file | diff | annotate |
| 2005-10-19 |
wenzelm |
2005-10-19 |
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
|
file | diff | annotate |
| 2005-10-19 |
mengj |
2005-10-19 |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file | diff | annotate |
| 2005-10-11 |
wenzelm |
2005-10-11 |
tuned;
|
file | diff | annotate |
| 2005-10-08 |
wenzelm |
2005-10-08 |
Poplog/PML: ML_SUFFIX=.psv;
|
file | diff | annotate |
| 2005-10-05 |
wenzelm |
2005-10-05 |
added Poplog/PML version 15.6/2.1 (experimental!);
|
file | diff | annotate |
| 2005-09-21 |
wenzelm |
2005-09-21 |
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
|
file | diff | annotate |
| 2005-09-20 |
webertj |
2005-09-20 |
pointers to src/HOL/Tools/sat_solver.ML added in comments
|
file | diff | annotate |
| 2005-09-14 |
wenzelm |
2005-09-14 |
no longer prefer xemacs, which fails more often than GNU emacs;
|
file | diff | annotate |
| 2005-08-18 |
wenzelm |
2005-08-18 |
tuned;
|
file | diff | annotate |
| 2005-08-16 |
wenzelm |
2005-08-16 |
-V outline=/proof,/ML;
|
file | diff | annotate |
| 2005-08-02 |
wenzelm |
2005-08-02 |
tuned ML_OPTIONS;
|
file | diff | annotate |
| 2005-08-02 |
wenzelm |
2005-08-02 |
tuned;
|
file | diff | annotate |
| 2005-08-01 |
wenzelm |
2005-08-01 |
polyml: use polyml-platform/version from Isabelle distribution;
removed DEFS_CHAIN_HISTORY;
|
file | diff | annotate |
| 2005-08-01 |
obua |
2005-08-01 |
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
|
file | diff | annotate |
| 2005-07-19 |
wenzelm |
2005-07-19 |
retract accidental user commit;
removed obsolete XSYMBOL_HOME;
tuned;
|
file | diff | annotate |
| 2005-07-19 |
obua |
2005-07-19 |
proving bounds for real linear programs
|
file | diff | annotate |
| 2005-07-12 |
avigad |
2005-07-12 |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy
|
file | diff | annotate |
| 2005-06-17 |
wenzelm |
2005-06-17 |
updated;
|
file | diff | annotate |
| 2005-06-05 |
wenzelm |
2005-06-05 |
#SMLNJ_CYGWIN_RUNTIME=1
|
file | diff | annotate |
| 2005-06-02 |
wenzelm |
2005-06-02 |
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
tuned;
|
file | diff | annotate |
| 2005-05-17 |
wenzelm |
2005-05-17 |
removed ISAMODE settings;
|
file | diff | annotate |
| 2005-04-29 |
haftmann |
2005-04-29 |
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
|
file | diff | annotate |
| 2005-04-29 |
haftmann |
2005-04-29 |
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
|
file | diff | annotate |
| 2005-04-27 |
gagern |
2005-04-27 |
removed --version which is not a valid polyml flag and has no effect
|
file | diff | annotate |
| 2005-04-26 |
wenzelm |
2005-04-26 |
reverted accidental commit of user modification;
|
file | diff | annotate |
| 2005-04-20 |
gagern |
2005-04-20 |
Fix automatic determination of poly version.
|
file | diff | annotate |
| 2005-04-20 |
quigley |
2005-04-20 |
Removed remaining references to Main.thy in reconstruction code.
|
file | diff | annotate |
| 2005-04-14 |
aspinall |
2005-04-14 |
Include automatic determination of poly version.
|
file | diff | annotate |
| 2005-04-13 |
wenzelm |
2005-04-13 |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;
|
file | diff | annotate |
| 2005-04-13 |
wenzelm |
2005-04-13 |
*** empty log message ***
|
file | diff | annotate |
| 2005-03-04 |
skalberg |
2005-03-04 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| 2005-02-06 |
paulson |
2005-02-06 |
fixed mac line
|
file | diff | annotate |