new lemma

more up-to-date error msg

\<dots> replaced by ...

refute

Documentation updated

Refute_Examples added/fixed

look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only if no multi platform installation found.

SML/NJ compatibility fixes

added Refute_Examples.thy

changed default values for refute

*** empty log message ***

support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps

Updated examples

*** empty log message ***

Internal and external SAT solvers

Formulas of propositional logic

ZCHAFF_HOME variable added

new thm

strengthened the axclass claims

suggest -p 1 proof object level for HOL

include more explanation of variables

*** empty log message ***

Bug-fixes for transitivity reasoner.

Added documentation for transitivity solver setup.

generic theorems about exponentials; general tidying up

new theory of infinite sets

Lex: removed last ML files

Conversion ML -> Isar

tweaked for times_ac1

tweaks

some new results

some new results

Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal

patch to NumberTheory problems caused by Parity

do not remove heaps, used for afp test

Lex: ML -> thy

ML -> Isar

new material from Avigad, and simplified treatment of division by 0

Removed ML files from Lex

Conversion of ML files to Isar.

added record_ex_sel_eq_simproc

fixed bugs in the setup of arithmetic procedures

converted Hyperreal/IntFloor to Isar script

tuned. proofs still gruesome..

converted MiniML to Isar

converted to Isar

new Ring_and_Field hierarchy, eliminating redundant axioms

converted Hyperreal/HTranscendental to Isar script

converted to Isar

union/intersection over intervals

Added specific code generator for number_of.

converted Hyperreal/Series to Isar script

converted Hyperreal/NatStar to Isar script

corrected authors

converted Hyperreal/HSeries to Isar script

find_tname now handles parameter renaming properly ("as they are printed").

converted Hyperreal/Log and Hyperreal/HLog to Isar scripts

converted NSCA to Isar script

converted HOL/Complex/NSInduct to Isar script

converted HOL/Complex/NSCA to Isar script

conversion of Complex/CStar to Isar script

conversion of Complex/CSeries to Isar script

conversion of Complex/CLim to Isar script

Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.

new "where" section

moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy

removal of the legacy ML structure List

new numerics section using type classes

New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.

Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.

moved list_all2I to List.thy

removed a reference to the ML structure List.thy

new theorem

comments!!

new Union syntax

removed obsolete theorem

Moved application of flexflex_unique from standard' to standard.

further tweaks to the numeric theories

arith

lemmas about card (set xs)

Polymorphic treatment of binary arithmetic using axclasses

Removed dangling exception handler

Missing } inserted

Removed "duplicate fact binding" error message.

Printing functions now use cond_extrn instead of extrn (due to short_names flag)

Added flag short_names

Modified UN and INT xsymbol syntax: made index subscript

*** empty log message ***

updated links to the old ftp site

generic of_nat and of_int functions, and generalization of iszero and neg

tidying up, especially the Complex numbers

Changed variable names.

*** empty log message ***

further tidying of the complex numbers

tidying of the complex numbers

Finally fixed the counterexample finder. Can now deal with < on real.

Conversion of HyperNat to Isar format and its declaration as a semiring

simplifications in the hyperreals

tidying up arithmetic for the hyperreals

converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.

remove more files (index, log files) for -c option

replacing HOL/Real/PRat, PNat by the rational number development > of Markus Wenzel

replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel

\<^raw...> does no longer print an additional space.

Reduced space for xsymbols output of [| |] ==> from 3 to 1

\\<...> will be converted to \<...> \\<^...> will be converted to \<^...>

* Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy

Added an exception handler and error msg.

Added print translation for pairs

cleaning up

print translation for ALL x <= n. P x

fixed old bugs in "decomp" (conversion from term to lin.arith. format). updated instantiation of real lin.arith.

Told linear arithmetic package about injections "real" from nat/int into real.

types complex and hcomplex are now instances of class ringpower: omitting redundant lemmas

Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers

Modified real arithmetic simplification

Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'

Adding 'refute' to HOL.

'refute', 'refute_params'.

Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal

set isasep to {} by default

Added lazy sequences and parser combinators for same.

separate thm lists in latex output by \isasep

run makeindex if necessary

map_idI

auto update

Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.

correction to cterm_instantiate by Christoph Leuth