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
2003-12-23 paulson 2003-12-23 new theorems
2003-12-23 paulson 2003-12-23 tidying up hcomplex arithmetic
2003-12-23 paulson 2003-12-23 renaming some theorems
2003-12-23 paulson 2003-12-23 type hcomplex is now in class field
2003-12-23 paulson 2003-12-23 more ML bindings
2003-12-23 kleing 2003-12-23 added some [intro?] and [trans] for list_all2 lemmas
2003-12-22 nipkow 2003-12-22 Updated proofs due to changes in Set.thy.
2003-12-22 paulson 2003-12-22 converted Complex/NSComplex to Isar script
2003-12-22 paulson 2003-12-22 removal of the abel_cancel simproc for hypreal
2003-12-22 paulson 2003-12-22 downgrading abel_cancel
2003-12-22 paulson 2003-12-22 new binding
2003-12-22 paulson 2003-12-22 simplifying
2003-12-22 paulson 2003-12-22 moving HyperArith0.ML to other theories
2003-12-22 paulson 2003-12-22 removing obsolete bindings
2003-12-21 paulson 2003-12-21 tidying of HOL/Auth esp Guard lemmas
2003-12-21 nipkow 2003-12-21 removed insert_Diff_single from simpset because it interfered with Auth :-(
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2003-12-19 paulson 2003-12-19 minor tweaks
2003-12-19 paulson 2003-12-19 type hypreal is an ordered field
2003-12-19 nipkow 2003-12-19 *** empty log message ***