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

Made sure all lemmas now have names (especially so that certain of them
2005-09-26, by skalberg
echo HOL_USERDIR_OPTIONS;
2005-09-26, by wenzelm
tuned
2005-09-26, by obua
added ROOT.ML
2005-09-26, by obua
adjusted web link
2005-09-26, by haftmann
added entry for running HOLLight
2005-09-26, by obua
fixed disambiguation problem
2005-09-26, by obua
added Drule.disambiguate_frees : thm -> thm
2005-09-26, by obua
zero_var_inst: replace loose bounds :000 etc.;
2005-09-25, by wenzelm
* Hyperreal: A theory of Taylor series.
2005-09-25, by wenzelm
more;
2005-09-25, by wenzelm
eq_codegen now ensures that code for bool type is generated.
2005-09-25, by berghofe
Fixed print mode problem in test_term.
2005-09-25, by berghofe
Added ExecutableSet and Taylor.
2005-09-25, by berghofe
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

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

isabelle