2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2004-02-19 paulson 2004-02-19 new numerics section using type classes
2004-02-19 ballarin 2004-02-19 New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-19 paulson 2004-02-19 moved list_all2I to List.thy
2004-02-19 paulson 2004-02-19 removed a reference to the ML structure List.thy
2004-02-19 paulson 2004-02-19 new theorem
2004-02-19 paulson 2004-02-19 comments!!
2004-02-18 paulson 2004-02-18 new Union syntax
2004-02-18 paulson 2004-02-18 removed obsolete theorem
2004-02-17 berghofe 2004-02-17 Moved application of flexflex_unique from standard' to standard.
2004-02-17 paulson 2004-02-17 further tweaks to the numeric theories
2004-02-16 paulson 2004-02-16 arith
2004-02-16 kleing 2004-02-16 lemmas about card (set xs)
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-14 nipkow 2004-02-14 Removed dangling exception handler
2004-02-12 nipkow 2004-02-12 Missing } inserted
2004-02-11 berghofe 2004-02-11 Removed "duplicate fact binding" error message.
2004-02-11 berghofe 2004-02-11 Printing functions now use cond_extrn instead of extrn (due to short_names flag)
2004-02-11 berghofe 2004-02-11 Added flag short_names
2004-02-11 nipkow 2004-02-11 Modified UN and INT xsymbol syntax: made index subscript
2004-02-11 nipkow 2004-02-11 *** empty log message ***
2004-02-10 paulson 2004-02-10 updated links to the old ftp site
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2004-02-05 paulson 2004-02-05 tidying up, especially the Complex numbers
2004-02-05 nipkow 2004-02-05 Changed variable names.
2004-02-04 nipkow 2004-02-04 *** empty log message ***
2004-02-03 paulson 2004-02-03 further tidying of the complex numbers
2004-02-03 paulson 2004-02-03 tidying of the complex numbers
2004-02-03 nipkow 2004-02-03 Finally fixed the counterexample finder. Can now deal with < on real.
2004-02-02 paulson 2004-02-02 Conversion of HyperNat to Isar format and its declaration as a semiring
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2004-01-28 kleing 2004-01-28 remove more files (index, log files) for -c option
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development > of Markus Wenzel
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-27 schirmer 2004-01-27 \<^raw...> does no longer print an additional space.
2004-01-27 nipkow 2004-01-27 Reduced space for xsymbols output of [| |] ==> from 3 to 1
2004-01-26 schirmer 2004-01-26 \\<...> will be converted to \<...> \\<^...> will be converted to \<^...>
2004-01-26 schirmer 2004-01-26 * 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
2004-01-25 nipkow 2004-01-25 Added an exception handler and error msg.
2004-01-20 schirmer 2004-01-20 Added print translation for pairs
2004-01-20 schirmer 2004-01-20 cleaning up
2004-01-14 kleing 2004-01-14 print translation for ALL x <= n. P x
2004-01-14 nipkow 2004-01-14 fixed old bugs in "decomp" (conversion from term to lin.arith. format). updated instantiation of real lin.arith.
2004-01-14 nipkow 2004-01-14 Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-13 paulson 2004-01-13 types complex and hcomplex are now instances of class ringpower: omitting redundant lemmas
2004-01-12 paulson 2004-01-12 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
2004-01-12 paulson 2004-01-12 Modified real arithmetic simplification
2004-01-12 webertj 2004-01-12 Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.
2004-01-10 webertj 2004-01-10 'refute', 'refute_params'.
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-09 kleing 2004-01-09 set isasep to {} by default
2004-01-08 skalberg 2004-01-08 Added lazy sequences and parser combinators for same.
2004-01-08 kleing 2004-01-08 separate thm lists in latex output by \isasep
2004-01-08 kleing 2004-01-08 run makeindex if necessary
2004-01-07 kleing 2004-01-07 map_idI
2004-01-06 paulson 2004-01-06 auto update