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
2004-01-06 paulson 2004-01-06 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.
2004-01-06 paulson 2004-01-06 correction to cterm_instantiate by Christoph Leuth
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2004-01-05 nipkow 2004-01-05 undid split_comp_eq[simp] because it leads to nontermination together with split_def!
2004-01-03 paulson 2004-01-03 Deleting more redundant theorems
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-29 kleing 2003-12-29 \<^bsub> .. \<^esub>
2003-12-29 kleing 2003-12-29 spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-25 nipkow 2003-12-25 Added trace msg
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-12-24 kleing 2003-12-24 list_all2_nthD no good as [intro?]
2003-12-23 kleing 2003-12-23 list_all2_mono should not be [trans]
2003-12-23 paulson 2003-12-23 reorganised complex arithmetic
2003-12-23 paulson 2003-12-23 removing real_of_posnat
2003-12-23 paulson 2003-12-23 converting Hyperreal/NthRoot to Isar
2003-12-23 paulson 2003-12-23 converting Complex/Complex.ML to Isar
2003-12-23 paulson 2003-12-23 deleting redundant theorems