added conf/ to .cvsignore

Add icon for interface.

Move welcomemsg and helpdoc to pgip_isar.xml

Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.

Explanatory text

Schema files (for information, and validating pgip_isar.xml)

Schema for PGIP

pruned notes about Poly/ML; removed unnecessary rename of Isabelle executable;

converted to Isar theory format;

Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.

tuned;

Fix for guiconfig -> displayconfig element rename

theorems need names

refer to $PRG instead of (old) rsync-isabelle;

updated;

updated;

pdfsetup.sty: better not rely on ifpdf.sty;

simprules need names

export debug_bounds;

explicit dependencies of SAT vs. Refute; removed unused methods;

explicit dependencies of SAT vs. Refute; moved late refute setup to SAT;

Isabelle2005 (October 2005); pdfsetup.sty now requires ifpdf.sty; added Simplifier.debug_bounds; do not advertize Simplifier.add_context_simprocs etc., which are to be replaced soon;

Added a few lemmas

reduction in tracing files

improvements for problem generation

moved concat_with_and to watcher.ML

a name for empty_not_insert

Simplifier now removes flex-flex constraints from theorem returned by prover.

Optimized and exported flexflex_unique.

make signature constraint actually work;

activate signature constraints;

HOL4 image is back;

tuned default operation: use internal modify;

abstract_rule: tuned exception msgs;

back to simple 'defs' (cf. revision 1.79 of theory.ML); renamed 'finals' to 'specified', share bookkeeping with defs; added monomorphic;

back to simple 'defs' (cf. revision 1.79); prep_const: Compress.type;

removed revert_bound; added debug_bounds flag;

print_theory: discontinued final consts;

Theory.add_finals_i;

more finalconsts;

tuned;

pointer to HOL/ex/SAT_Examples.thy added

updated;

more reliable check for PDF output using ifpdf.sty;

pre_sat_tac moved towards end of file

adjusted www links

comment fixed

mapped "-->" to "hol4-->"

avoid naming existing tags in explanations;

revert 'defs' advertisement;

revert 'defs' advertisement; removed PG/xemacs note, which is actually wrong now; tuned;

time limit option; fixed bug concerning first line of ATP output

streamlined theory; conformance to recent publication

new lemma

better appearance in lynx and netscape4

MB instead of KB

renamed packages to download;

more details about incomplete 'defs';

renamed "Packages" to "Download";

build bed

build bed

build bed

slight corrections

tuned;

renamed "Packages" to "Download";

fixed dead link

fixed dead link

improved linkcheck

added simple linktester for isabelle website

warn about Poly/ML segfault problem;

website preparation for Isabelle2005

corrected spelling bug

added defs disclaimer

nat_number_of is no longer declared as code lemma, since this turned out to be too inefficient.

Inserted clause for nat in number_of_codegen again ("code unfold" turned out to be too inefficient).

Optimized unfold_attr.

removed link to HOL4, which is not in the library right now;

tuned;

Added entries for code_module, code_library, and value.

Tuned.

updates for Isabelle2005;

tuned;

Updated description of code generator.

updated;

moved disambiguate_frees to ProofKernel;

quote 'value';

yet another atempt to get doc/Contents right;

Renamed wf_rec to wfrec in consts_code declaration.

really copy doc/Contents;

Release HOL4 and HOLLight Importer.

copy doc/Contents;

Made sure all lemmas now have names (especially so that certain of them can be removed from the simpset).

echo HOL_USERDIR_OPTIONS;

tuned

added ROOT.ML

adjusted web link

added entry for running HOLLight

fixed disambiguation problem

added Drule.disambiguate_frees : thm -> thm

zero_var_inst: replace loose bounds :000 etc.;

* Hyperreal: A theory of Taylor series.

more;

eq_codegen now ensures that code for bool type is generated.

Fixed print mode problem in test_term.

Added ExecutableSet and Taylor.

Now uses set implementation from ExecutableSet.

Added Taylor.

Formalization of Taylor series by Lukas Bulwahn and Bernhard Haeupler.

Added ExecutableSet.

New theory for implementing finite sets by lists.

sat_solver.ML not loaded anymore (already loaded by Refute.thy)

set show_types and show_sorts during import

a few new filter lemmas

HOL4-Import: map ONTO to Fun.surj

cnf_struct renamed to cnf

remove debug clutter

preliminary fix of HOL build problem

bug fix

replay_proof optimized: now performs backwards proof search

code reformatted and restructured, many minor modifications

bugfix in "zchaff_with_proofs"

parse_std_result_file renamed to read_std_result_file

new sat tactic

new sat tactic imports resolution proofs from zChaff

fix

simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);

tuned msg;

added mk_solver'; export revert_bounds; check_bounds if debug_simp;

Simplifier.inherit_bounds;

adm_tac/cont_tacRs: proper simpset;

Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;

tuned order of targets;

Provers/cancel_sums.ML: Simplifier.inherit_bounds;

some typos in comments fixed

1) fixed bug in type_introduction: first stage uses different namespace than second stage 2) fixed bug in dump_import_thy via gen2replay function

removed doc/index.html from distribution (now produced by website);

mkdir -p for symlinks

rules -> iprover

spaces inserted in header

header (title/ID) added

typo fixed: rufute -> refute

bugfix in record_tr'

method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;

Id;

tuned;

changed defaults

ATP linkup

replay type_introduction fix

temporarily re-introduced overwrite_warn

add debug messages

renamed rules to iprover

*** empty log message ***

renamed rules to iprover

fix because of list lemmas

renamed "rules" to "iprover"

added theorem adm_ball

cleaned up

HOLCF theorem naming conventions

removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements

Fix because of new lemma in List

solver "auto" does not reverse the list of solvers anymore

added fold_map_graph

added fold_map_table

only show trunk in Changelog (kleing)

zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore

echo HOL_USEDIR_OPTIONS;

tuned;

PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);

updated for Isabelle2005;

tuned;

updated for Isabelle2005;

obsolete;

improved proof parsing

trying to limit the looping

updated for Isabelle2005;

new header syntax;

introduces update_warn instead of overwrite_warn

added AList.make, eq_fst, apr ...

unify dist and main

tuned;

fixed cvs export;

tuned;

obsolete;

tuned;

the_default, the_list;

updated;

quote "value";

removed "--" argument; updated for Isabelle2005; tuned;

isatool fixheaders;

Added new "value" command.

Simplified code generator for numerals.

Declared nat_number_of as code lemma.

- Added eval_term function and value command - Fixed name clash problem in test_term

tunes;

updated for Isabelle2005;

HOL-Complex-Matrix: fixed deps;

tuned;

updated for Isabelle2005;

tuned;

(name mess cleanup)

introduced AList module

removed assoc, overwrite

added update_warn

tuned;

fixed proof script of lemma merges_same_conv (Why did it stop working?);

updated;

tuned;

HOL/ex/Chinese.thy;

tuned;

more contributions;

tuned headers;

tuned header;

use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;

fixed proof script of lemma Cond_sound (Why did it stop working anyway?);

bugfix in "zchaff_with_proofs"

fixed recursive-looking declaration

tidying, and support for axclass/classrel clauses

fixed syntax for sml/nj

undone the previous change: show_hyps not supported anymore

pointers to src/HOL/Tools/sat_solver.ML added in comments

introduced AList module in favor of assoc etc.

new menu item show-sort-hypotheses to toggle show_hyps

HOL/ex/Chinese.thy; PROOFGENERAL_OPTIONS: no longer prefer xemacs;

HOL-ex: Library/Commutative_Ring.thy;

moved Tools/comm_ring.ML to Library;

added Commutative_Ring (from Main HOL);

Simplifier.inherit_bounds;

TextIO.inputLine: handle IO.Io, assuming it stems from a signal;

get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;

removed obsolete thms_containing;

tuned;

tuned simprocs;

removed Commutative_Ring hacks;

tuned theory dependencies;

removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;

tuned;

Chinese Unicode example;

tuned proofs;

The simpset of the actual theory is take, in order to handle rings defined after the method

further tidying; killing of old Watcher loops