*** empty log message ***

Replaced `div and `mod in consts_code section by div and mod.

bugfix in read_dimacs_cnf_file

Disallowed "includes" in locale declarations.

Fixed bug in compile_clause that caused equality constraints to be "forgotten".

warning for recursion over IDTs added

Aded a thm.

*** empty log message ***

proof_of_evalc corrected;

Initial changes to extend arithmetic from individual types to type classes.

undid UN/INT syntax

undid UN/INT xsymbol syntax with subscripts.

make_clauses now meta

RS -> THEN

modified resolution proof

Undid \Union syntax with subscripts.

an updated treatment of the simprules

some structured proofs

added a thm

added some inj_on thms

Added a number of new thms and the new function remove1

proof mod

added a few thms

oracle corrected

aded comment

fixed tex problem

Typo.

New transitivity reasoners for transitivity only and quasi orders.

new simprules Int_subset_iff and Un_subset_iff

zdiv_int, zmod_int

conversion of Hyperreal/Filter to Isar scripts

Some comments added.

Documentation added/improved.

Modifications for trancl_tac (new solver in simplifier).

Documentation added; minor improvements.

Theories now take advantage of recent syntax improvements with (structure).

conversion of Hyperreal/{Fact,Filter} to Isar scripts

conversion of Integration and NSPrimes to Isar scripts

keep type_solver;

tuned dependencies;

added context type solver;

ZF/Simplifier: second copy of context type solver;

tuned output;

- optimized nodup_vars check in capply - new function dest_ctyp

removal of more iff-rules from RealDef.thy

removed some [iff] declarations from RealDef.thy, concerning inequalities

tidied

documents for ZF-AC and ZF-Constructible

conversion of SEQ.ML to Isar script

abs notation

fixed precedences

conversion of Hyperreal/MacLaurin_lemmas to Isar script

*** empty log message ***

converting Hyperreal/Transcendental to Isar script

New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver

minor formatting fixes

Modified \<Sum> syntax a little.

*** empty log message ***

new material courtesy of Norbert Voelker

updated;

Fixed latex problem

ring_1 -> ring

minor tweaks to go with the new version of the Accountability paper

removed some obsolete proofs

two new results

Some changes to allow qualified theory import.

- Moved code generator setup for lists from Main.thy to List.thy - Code generator now represents char type as strings of length 1 (easier to handle than encoding using nibbles)

Moved code generator setup for lists to List.thy

Added function dest_list.

Added simple check that allows code generator to produce code containing fewer redundant matches.

Added function unprefix.

tuned

added: get_extT_fields and get_recT_fields

added Complex/root

Fine-tuned sum syntax.

Corrected TeX problem.

Created.

Corrected TeX problems.

Added nice latex syntax.

int_ord = Int.compare, string_ord = String.compare;

*** empty log message ***

more summation syntax

more syntax

redefining sumr to be a translation to setsum

*** empty log message ***

Moved to new m<..<n syntax for set intervals.

*** empty log message ***

?

added {0::nat..n(} = {..n(}

Got rid of Summation and made it a translation into setsum instead.

read_dimacs_cnf_file added

added README

corrected bibtex entry

*** empty log message ***

context dependent components;

added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;

improved print_ss; tuned;

Simplifier and Classical Reasoner now support proof context dependent plug-ins;

local_cla/simpset_of;

- Added support for conditional equations whose premises involve inductive sets (useful in connection with THE operator) - Inductive and non-inductive sets (implemented as lists) can now be mixed

- Expressed infer_derivs' in terms of infer_deriv - Eta-expanded function instantiate to delay evaluation (avoids inefficiencies when proof terms are switched off)

- 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;

added PRINT_COMMAND setting

added isatool display and isatool print;

print document

display document (in DVI format)

root for draft documents;

Library.translate_string;

added trace (inefficient for very long input);

added translate_string;

added read (provides transition names and sources);

added output_known_symbols; tuned;

added name_of, source_of, source;

added Present.drafts;

added option 'isatool latex -o syms';

An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.

tuned;

improved RemoteFile;

tuned;

Removed this: not really ready yet.

Interface configuration for Isar

Sign.is_logtype;

prs: Output.output;

added split_ext; removed drop_ext;

tuned comment;

Scan.this_string;

tuned representation; added RemoteFile;

tuned;

added this_string;

tuned messages;

added is_logtype (replaces logtypes field of syntax); tuned merge;

removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;

removed separate logtypes field of syntax;

Path.split_ext; more robust inform_file_processed;

Sign.is_logtype;

Syntax.default_mode;

added option 'locale=NAME';

Url.File;

* Document preparation: antiquotations provide option 'locale=NAME';

tuned comment;

updated/tuned identifier syntax;

updated notes on sub-/superscripts;

removed Syntax.test_read;

added a lemma lfp_ordinal_induct

fixed the groupI ambiguity