Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-256
+256
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
renamed "Packages" to "Download";
2005-09-27, by wenzelm
fixed dead link
2005-09-27, by haftmann
fixed dead link
2005-09-27, by haftmann
improved linkcheck
2005-09-27, by haftmann
added simple linktester for isabelle website
2005-09-27, by haftmann
warn about Poly/ML segfault problem;
2005-09-27, by wenzelm
website preparation for Isabelle2005
2005-09-27, by haftmann
corrected spelling bug
2005-09-27, by obua
added defs disclaimer
2005-09-27, by obua
nat_number_of is no longer declared as code lemma, since this turned
2005-09-27, by berghofe
Inserted clause for nat in number_of_codegen again ("code unfold" turned
2005-09-27, by berghofe
Optimized unfold_attr.
2005-09-27, by berghofe
removed link to HOL4, which is not in the library right now;
2005-09-27, by wenzelm
tuned;
2005-09-27, by wenzelm
Added entries for code_module, code_library, and value.
2005-09-27, by berghofe
Tuned.
2005-09-27, by berghofe
updates for Isabelle2005;
2005-09-26, by wenzelm
tuned;
2005-09-26, by wenzelm
Updated description of code generator.
2005-09-26, by berghofe
updated;
2005-09-26, by wenzelm
moved disambiguate_frees to ProofKernel;
2005-09-26, by wenzelm
quote 'value';
2005-09-26, by wenzelm
yet another atempt to get doc/Contents right;
2005-09-26, by wenzelm
Renamed wf_rec to wfrec in consts_code declaration.
2005-09-26, by berghofe
really copy doc/Contents;
2005-09-26, by wenzelm
Release HOL4 and HOLLight Importer.
2005-09-26, by obua
copy doc/Contents;
2005-09-26, by wenzelm
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
*** 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
echo HOL_USEDIR_OPTIONS;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
obsolete;
2005-09-21, by wenzelm
improved proof parsing
2005-09-21, by paulson
trying to limit the looping
2005-09-21, by paulson
updated for Isabelle2005;
2005-09-21, by wenzelm
new header syntax;
2005-09-21, by wenzelm
introduces update_warn instead of overwrite_warn
2005-09-21, by haftmann
added AList.make, eq_fst, apr ...
2005-09-21, by haftmann
unify dist and main
2005-09-21, by haftmann
tuned;
2005-09-21, by wenzelm
fixed cvs export;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
obsolete;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
the_default, the_list;
2005-09-21, by wenzelm
updated;
2005-09-21, by wenzelm
quote "value";
2005-09-21, by wenzelm
removed "--" argument;
2005-09-21, by wenzelm
isatool fixheaders;
2005-09-21, by wenzelm
Added new "value" command.
2005-09-21, by berghofe
Simplified code generator for numerals.
2005-09-21, by berghofe
Declared nat_number_of as code lemma.
2005-09-21, by berghofe
- Added eval_term function and value command
2005-09-21, by berghofe
tunes;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
HOL-Complex-Matrix: fixed deps;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
(name mess cleanup)
2005-09-21, by haftmann
introduced AList module
2005-09-21, by haftmann
removed assoc, overwrite
2005-09-21, by haftmann
added update_warn
2005-09-21, by haftmann
tuned;
2005-09-21, by wenzelm
fixed proof script of lemma merges_same_conv (Why did it stop working?);
2005-09-20, by wenzelm
updated;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
more contributions;
2005-09-20, by wenzelm
tuned headers;
2005-09-20, by wenzelm
tuned header;
2005-09-20, by wenzelm
use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;
2005-09-20, by wenzelm
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
2005-09-20, by wenzelm
bugfix in "zchaff_with_proofs"
2005-09-20, by webertj
fixed recursive-looking declaration
2005-09-20, by paulson
tidying, and support for axclass/classrel clauses
2005-09-20, by paulson
fixed syntax for sml/nj
2005-09-20, by paulson
undone the previous change: show_hyps not supported anymore
2005-09-20, by webertj
pointers to src/HOL/Tools/sat_solver.ML added in comments
2005-09-20, by webertj
introduced AList module in favor of assoc etc.
2005-09-20, by haftmann
new menu item show-sort-hypotheses to toggle show_hyps
2005-09-20, by webertj
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
HOL-ex: Library/Commutative_Ring.thy;
2005-09-20, by wenzelm
moved Tools/comm_ring.ML to Library;
2005-09-20, by wenzelm
added Commutative_Ring (from Main HOL);
2005-09-20, by wenzelm
Simplifier.inherit_bounds;
2005-09-20, by wenzelm
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
2005-09-20, by wenzelm
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
2005-09-20, by wenzelm
removed obsolete thms_containing;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
tuned simprocs;
2005-09-20, by wenzelm
removed Commutative_Ring hacks;
2005-09-20, by wenzelm
tuned theory dependencies;
2005-09-20, by wenzelm
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
Chinese Unicode example;
2005-09-20, by wenzelm
tuned proofs;
2005-09-20, by wenzelm
The simpset of the actual theory is take, in order to handle rings defined after the method
2005-09-20, by chaieb
further tidying; killing of old Watcher loops
2005-09-20, by paulson
added a number of lemmas
2005-09-20, by nipkow
uniform handling of interrupts
2005-09-20, by paulson
algebra method added.
2005-09-20, by chaieb
improved eq_fst and eq_snd, removed some deprecated stuff
2005-09-20, by haftmann
added make and find
2005-09-20, by haftmann
slight adaptions to library changes
2005-09-20, by haftmann
infix operator precedence
2005-09-20, by haftmann
using curried Inttab.update_new function now
2005-09-20, by webertj
SAT solver interface modified to support proofs of unsatisfiability
2005-09-19, by webertj
shrink: compress terms and types;
2005-09-19, by wenzelm
added String.isSuffix;
2005-09-19, by wenzelm
maybe the last bug fix (sigh)?
2005-09-19, by obua
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19, by obua
further simplification of the Isabelle-ATP linkup
2005-09-19, by paulson
added make function
2005-09-19, by haftmann
removed some deprecated assocation list functions
2005-09-19, by haftmann
introduced AList module
2005-09-19, by haftmann
simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-19, by paulson
update usage message
2005-09-19, by kleing
obsolete;
2005-09-19, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
moved quick_and_dirty to Pure/ROOT.ML;
2005-09-17, by wenzelm
pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17, by wenzelm
added quick_and_dirty (from Isar/skip_proofs.ML);
2005-09-17, by wenzelm
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-17, by wenzelm
tuned comments;
2005-09-17, by wenzelm
pretty_thm_aux: aconv hyps;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
Hebrew: HTML.with_charset;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
added quickcheck_params (from Main.thy);
2005-09-17, by wenzelm
removed spurious PolyML.exception_trace;
2005-09-17, by wenzelm
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-17, by wenzelm
minor cleanup, moved stuff in its proper place;
2005-09-17, by wenzelm
generate: added HOL-Complex-Generate-HOLLight;
2005-09-17, by wenzelm
added code generator setup (from Main.thy);
2005-09-17, by wenzelm
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2005-09-17, by wenzelm
HTML.with_charset;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
obsolete;
2005-09-17, by wenzelm
plain test session, includes example;
2005-09-17, by wenzelm
theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-17, by wenzelm
added auto_fix (from proof.ML);
2005-09-17, by wenzelm
export put_facts;
2005-09-17, by wenzelm
interpretation: use goal commands without target -- no storing of results;
2005-09-17, by wenzelm
theorem(_i): empty target;
2005-09-17, by wenzelm
pretty_thm_aux: observe asms context;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
Cube: converted to Isar, use locales;
2005-09-17, by wenzelm
1) mapped .. and == constants
2005-09-17, by obua
use interpretation command
2005-09-17, by huffman
add HOLCF entries for pcpodef, cont_proc, fixrec;
2005-09-16, by huffman
converted to Isar theory format;
2005-09-16, by wenzelm
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-09-16, by obua
add header
2005-09-16, by huffman
tuned
2005-09-16, by ballarin
interpretation uses primitive goal interface
2005-09-16, by ballarin
tuned
2005-09-16, by ballarin
PARTIAL conversion to Vampire8
2005-09-16, by paulson
catching exception Io
2005-09-16, by paulson
rearranged
2005-09-16, by huffman
use mem operator
2005-09-16, by huffman
fix names in hypreal_arith.ML
2005-09-16, by huffman
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
2005-09-15, by huffman
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-15, by huffman
add header
2005-09-15, by huffman
The SMLNJ Problem fixed...
2005-09-15, by chaieb
getting it work for SMLNJ
2005-09-15, by chaieb
* Improved efficiency of the Simplifier etc.;
2005-09-15, by wenzelm
incorporated into NEWS;
2005-09-15, by wenzelm
incorporated HOL/Hyperreal/CHANGES;
2005-09-15, by wenzelm
massive tidy-up and simplification
2005-09-15, by paulson
less
more
|
(0)
-10000
-3000
-1000
-256
+256
+1000
+3000
+10000
+30000
tip