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 ***
2003-12-18 paulson 2003-12-18 tidied
2003-12-18 nipkow 2003-12-18 *** empty log message ***
2003-12-17 paulson 2003-12-17 converted Hyperreal/HyperDef to Isar script
2003-12-16 kleing 2003-12-16 fixed PG link
2003-12-16 paulson 2003-12-16 converted Hyperreal/HyperOrd to new-style theory
2003-12-15 paulson 2003-12-15 updated references to the now-pornographic proofgeneral.org
2003-12-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-12-13 paulson 2003-12-13 absolute value theorems moved to HOL/Ring_and_Field
2003-12-12 paulson 2003-12-12 moving some division theorems to Ring_and_Field
2003-12-12 kleing 2003-12-12 changed proof general links
2003-12-11 ballarin 2003-12-11 Change to prune_prems in Pure/Isar/locale.ML.
2003-12-11 paulson 2003-12-11 removal of abel_cancel from Real
2003-12-10 paulson 2003-12-10 combining Real/{RealArith0,real_arith}.ML
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type variables.
2003-12-10 ballarin 2003-12-10 New structure "partial_object" as common root for lattices and magmas.
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type vars.
2003-12-07 paulson 2003-12-07 re-organisation of Real/RealArith0.ML; more `Isar scripts
2003-12-06 kleing 2003-12-06 moreover and also do not reset facts any more
2003-12-06 kleing 2003-12-06 do not reset facts ('this') for moreover and also
2003-12-06 kleing 2003-12-06 make Pure first to avoid race conditions on multiprocessor machines
2003-12-06 kleing 2003-12-06 revert to 1.18, changed Distribution/lib/Tools/makeall instead
2003-12-06 kleing 2003-12-06 make Pure first to avoid race conditions on multi processor machines
2003-12-05 skalberg 2003-12-05 Added lazy sequences and parser combinators for same.
2003-12-05 paulson 2003-12-05 more field division lemmas transferred from Real to Ring_and_Field
2003-12-05 paulson 2003-12-05 stylistic changes
2003-12-05 paulson 2003-12-05 Converting more of the "real" development to Isar scripts
2003-12-04 nipkow 2003-12-04 hide Push
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-12-02 paulson 2003-12-02 More re-organising of numerical theorems
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals
2003-11-20 paulson 2003-11-20 conversion of Integ/Int_lemmas.ML to Isar script
2003-11-20 paulson 2003-11-20 including 0 ~= 1 in definition of Field
2003-11-19 paulson 2003-11-19 additions to Ring_and_Field
2003-11-18 paulson 2003-11-18 fixed a comment