| 2005-09-26 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-26 |
berghofe |
Updated description of code generator.
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
updated;
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
moved disambiguate_frees to ProofKernel;
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
quote 'value';
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
yet another atempt to get doc/Contents right;
|
changeset |
files
|
| 2005-09-26 |
berghofe |
Renamed wf_rec to wfrec in consts_code declaration.
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
really copy doc/Contents;
|
changeset |
files
|
| 2005-09-26 |
obua |
Release HOL4 and HOLLight Importer.
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
copy doc/Contents;
|
changeset |
files
|
| 2005-09-26 |
skalberg |
Made sure all lemmas now have names (especially so that certain of them
|
changeset |
files
|
| 2005-09-26 |
wenzelm |
echo HOL_USERDIR_OPTIONS;
|
changeset |
files
|
| 2005-09-26 |
obua |
tuned
|
changeset |
files
|
| 2005-09-26 |
obua |
added ROOT.ML
|
changeset |
files
|
| 2005-09-26 |
haftmann |
adjusted web link
|
changeset |
files
|
| 2005-09-26 |
obua |
added entry for running HOLLight
|
changeset |
files
|
| 2005-09-26 |
obua |
fixed disambiguation problem
|
changeset |
files
|
| 2005-09-26 |
obua |
added Drule.disambiguate_frees : thm -> thm
|
changeset |
files
|
| 2005-09-25 |
wenzelm |
zero_var_inst: replace loose bounds :000 etc.;
|
changeset |
files
|
| 2005-09-25 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
changeset |
files
|
| 2005-09-25 |
wenzelm |
more;
|
changeset |
files
|
| 2005-09-25 |
berghofe |
eq_codegen now ensures that code for bool type is generated.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Fixed print mode problem in test_term.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Added ExecutableSet and Taylor.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Now uses set implementation from ExecutableSet.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Added Taylor.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Formalization of Taylor series by Lukas Bulwahn and
|
changeset |
files
|
| 2005-09-25 |
berghofe |
Added ExecutableSet.
|
changeset |
files
|
| 2005-09-25 |
berghofe |
New theory for implementing finite sets by lists.
|
changeset |
files
|
| 2005-09-24 |
webertj |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
changeset |
files
|
| 2005-09-24 |
obua |
set show_types and show_sorts during import
|
changeset |
files
|
| 2005-09-24 |
nipkow |
a few new filter lemmas
|
changeset |
files
|
| 2005-09-24 |
obua |
HOL4-Import: map ONTO to Fun.surj
|
changeset |
files
|
| 2005-09-24 |
webertj |
cnf_struct renamed to cnf
|
changeset |
files
|
| 2005-09-24 |
obua |
remove debug clutter
|
changeset |
files
|
| 2005-09-24 |
obua |
preliminary fix of HOL build problem
|
changeset |
files
|
| 2005-09-24 |
obua |
bug fix
|
changeset |
files
|
| 2005-09-24 |
webertj |
replay_proof optimized: now performs backwards proof search
|
changeset |
files
|
| 2005-09-24 |
webertj |
code reformatted and restructured, many minor modifications
|
changeset |
files
|
| 2005-09-24 |
webertj |
bugfix in "zchaff_with_proofs"
|
changeset |
files
|
| 2005-09-24 |
webertj |
parse_std_result_file renamed to read_std_result_file
|
changeset |
files
|
| 2005-09-23 |
webertj |
new sat tactic
|
changeset |
files
|
| 2005-09-23 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
changeset |
files
|
| 2005-09-23 |
obua |
fix
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
tuned msg;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
added mk_solver';
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
Simplifier.inherit_bounds;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
adm_tac/cont_tacRs: proper simpset;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
tuned order of targets;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| 2005-09-23 |
webertj |
some typos in comments fixed
|
changeset |
files
|
| 2005-09-23 |
obua |
1) fixed bug in type_introduction: first stage uses different namespace than second stage
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
removed doc/index.html from distribution (now produced by website);
|
changeset |
files
|
| 2005-09-23 |
haftmann |
mkdir -p for symlinks
|
changeset |
files
|
| 2005-09-23 |
nipkow |
rules -> iprover
|
changeset |
files
|
| 2005-09-23 |
webertj |
spaces inserted in header
|
changeset |
files
|
| 2005-09-23 |
webertj |
header (title/ID) added
|
changeset |
files
|
| 2005-09-23 |
webertj |
typo fixed: rufute -> refute
|
changeset |
files
|
| 2005-09-23 |
schirmer |
bugfix in record_tr'
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
Id;
|
changeset |
files
|
| 2005-09-23 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-23 |
paulson |
changed defaults
|
changeset |
files
|
| 2005-09-23 |
paulson |
ATP linkup
|
changeset |
files
|
| 2005-09-23 |
obua |
replay type_introduction fix
|
changeset |
files
|
| 2005-09-23 |
haftmann |
temporarily re-introduced overwrite_warn
|
changeset |
files
|
| 2005-09-22 |
obua |
add debug messages
|
changeset |
files
|
| 2005-09-22 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| 2005-09-22 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2005-09-22 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| 2005-09-22 |
nipkow |
fix because of list lemmas
|
changeset |
files
|
| 2005-09-22 |
nipkow |
renamed "rules" to "iprover"
|
changeset |
files
|
| 2005-09-22 |
huffman |
added theorem adm_ball
|
changeset |
files
|
| 2005-09-22 |
huffman |
cleaned up
|
changeset |
files
|
| 2005-09-22 |
huffman |
HOLCF theorem naming conventions
|
changeset |
files
|
| 2005-09-22 |
paulson |
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
|
changeset |
files
|
| 2005-09-22 |
nipkow |
Fix because of new lemma in List
|
changeset |
files
|
| 2005-09-22 |
webertj |
solver "auto" does not reverse the list of solvers anymore
|
changeset |
files
|
| 2005-09-22 |
haftmann |
added fold_map_graph
|
changeset |
files
|
| 2005-09-22 |
haftmann |
added fold_map_table
|
changeset |
files
|
| 2005-09-21 |
isatest |
only show trunk in Changelog (kleing)
|
changeset |
files
|
| 2005-09-21 |
webertj |
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
echo HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
obsolete;
|
changeset |
files
|
| 2005-09-21 |
paulson |
improved proof parsing
|
changeset |
files
|
| 2005-09-21 |
paulson |
trying to limit the looping
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| 2005-09-21 |
wenzelm |
new header syntax;
|
changeset |
files
|
| 2005-09-21 |
haftmann |
introduces update_warn instead of overwrite_warn
|
changeset |
files
|