isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Now uses set implementation from ExecutableSet.
2005-09-25, by berghofe
Added Taylor.
2005-09-25, by berghofe
Formalization of Taylor series by Lukas Bulwahn and
2005-09-25, by berghofe
Added ExecutableSet.
2005-09-25, by berghofe
New theory for implementing finite sets by lists.
2005-09-25, by berghofe
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
2005-09-25, by webertj
set show_types and show_sorts during import
2005-09-24, by obua
a few new filter lemmas
2005-09-24, by nipkow
HOL4-Import: map ONTO to Fun.surj
2005-09-24, by obua
cnf_struct renamed to cnf
2005-09-24, by webertj
remove debug clutter
2005-09-24, by obua
preliminary fix of HOL build problem
2005-09-24, by obua
bug fix
2005-09-24, by obua
replay_proof optimized: now performs backwards proof search
2005-09-24, by webertj
code reformatted and restructured, many minor modifications
2005-09-24, by webertj
bugfix in "zchaff_with_proofs"
2005-09-24, by webertj
parse_std_result_file renamed to read_std_result_file
2005-09-24, by webertj
new sat tactic
2005-09-23, by webertj
new sat tactic imports resolution proofs from zChaff
2005-09-23, by webertj
fix
2005-09-23, by obua
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
2005-09-23, by wenzelm
tuned msg;
2005-09-23, by wenzelm
added mk_solver';
2005-09-23, by wenzelm
Simplifier.inherit_bounds;
2005-09-23, by wenzelm
adm_tac/cont_tacRs: proper simpset;
2005-09-23, by wenzelm
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
tuned order of targets;
2005-09-23, by wenzelm
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
some typos in comments fixed
2005-09-23, by webertj
1) fixed bug in type_introduction: first stage uses different namespace than second stage
2005-09-23, by obua
removed doc/index.html from distribution (now produced by website);
2005-09-23, by wenzelm
mkdir -p for symlinks
2005-09-23, by haftmann
rules -> iprover
2005-09-23, by nipkow
spaces inserted in header
2005-09-23, by webertj
header (title/ID) added
2005-09-23, by webertj
typo fixed: rufute -> refute
2005-09-23, by webertj
bugfix in record_tr'
2005-09-23, by schirmer
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
2005-09-23, by wenzelm
Id;
2005-09-23, by wenzelm
tuned;
2005-09-23, by wenzelm
changed defaults
2005-09-23, by paulson
ATP linkup
2005-09-23, by paulson
replay type_introduction fix
2005-09-23, by obua
temporarily re-introduced overwrite_warn
2005-09-23, by haftmann
add debug messages
2005-09-23, by obua
renamed rules to iprover
2005-09-23, by nipkow
*** empty log message ***
2005-09-23, by nipkow
renamed rules to iprover
2005-09-22, by nipkow
fix because of list lemmas
2005-09-22, by nipkow
renamed "rules" to "iprover"
2005-09-22, by nipkow
added theorem adm_ball
2005-09-22, by huffman
cleaned up
2005-09-22, by huffman
HOLCF theorem naming conventions
2005-09-22, by huffman
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
2005-09-22, by paulson
Fix because of new lemma in List
2005-09-22, by nipkow
solver "auto" does not reverse the list of solvers anymore
2005-09-22, by webertj
added fold_map_graph
2005-09-22, by haftmann
added fold_map_table
2005-09-22, by haftmann
only show trunk in Changelog (kleing)
2005-09-22, by isatest
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
2005-09-21, by webertj

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle