- Removed obsolete clause in function check_str - test_term now temporarily sets print_mode to [] as well

new profiling function

adapted type of simprocs;

make SML/NJ happy;

added add_term_varnames, term_varnames;

got rid of obsolete meta_simpset; tuned;

major cleanup; got rid of obsolete meta_simpset;

tuned simprocs;

got rid of obsolete meta_simpset;

tuned;

removed obsolete dependency;

* Pure/Namespace: flag unique_names added * Pure/Tactic: print_tac outputs goal through trace channel * HOL/Simplifier: extended record_upd_simproc

print_tac now outputs goals through trace-channel

added flag unique_names

* record_upd_simproc also simplifies trivial updates: r(|x := x r|) = r * tuned quick and dirty mode

Added delete operation.

new treatment of binary numerals

Added reference record_definition_quick_and_dirty_sensitive, to skip proofs triggered by a record definition, if quick_and_dirty is enabled.

Made simplification procedures simpset-aware.

license change to BSD

support for sparse matrices

new method for explicit classical resolution

auto update

Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.

Norbert Voelker

ringpower to recpower

replaced monomorphic abs definitions by abs_if

tidied

Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.

tuned;

faster conversion into DIMACS CNF and DIMACS SAT format

tuned;

tuned;

improved print_theory;

added output, removed pp_undef;

added chars_only, symbol_output;

tuned certify_typ/term;

tuned output;

added unparse;

pretty_abbr;

tuned certify_typ;

Type.cert_typ;

tuned certify_term;

added certify_class/sort;

added >>> : transition list -> unit;

immediate_output;

avoid \...\;

File.quote_sysify_path;

Merged in license change from Isabelle2004

got rid of Output.output for default print mode;

added checkTimer;

added accumulated timing;

added escape, export encode_raw, default mode now trivial, tuned;

use_output: Symbol.escape;

tuned pp;

avoid premature evaluation of syn_of (wastes time in conjunction with pp);

Symbol.encode_raw;

tuned;

improved comments -- required by 'isatool latex -o syms';

more generous treatment of packages in draft prints;

scalable string_of_tree; tuned;

tuned exists_string;

isatool_document: verbose option;

Add \usepackage{latexsym}

new SAT solver interface

improved defcnf conversion

removal of magmas and semigroups

fixed 'requires' comments, which are needed for printing of drafts;

isub/isup quasi letter (again); tuned;

tuned;

tuned

isatool_document: writeln output;

tuned document;

prevent looping of error messages involving malformed symbols;

tuned;

removed unused help function;

new fib example

removal of x-symbol syntax <Sigma> for dependent products

ISABELLE_TMP

path instead of string;

added path;

tuned lexical syntax;

num tokens;

fixed bad link

slight speed improvement

strengthened some theorems

Jerusat settings added

entries for ZChaff and BerkMin added/modified

Oracle corrected

Further development of matrix theory

faster defcnf conversion

updated;

updated;

tuned;

tuned Present.drafts;

added display_drafts and print_drafts commands;