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
2003-11-18 paulson 2003-11-18 new theorems for Rings
2003-11-18 paulson 2003-11-18 conversion of ML to Isar scripts
2003-11-18 berghofe 2003-11-18 Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors.
2003-11-14 ballarin 2003-11-14 Type inference bug in Isar attributes "where" and "of" fixed.
2003-11-12 paulson 2003-11-12 tidied
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
2003-10-31 kleing 2003-10-31 fixed
2003-10-31 kleing 2003-10-31 set isatool usedir to verbose by default
2003-10-30 paulson 2003-10-30 Got rid of the structure "Int", which was obsolete and which obscured the eponymous Basis Library structure
2003-10-29 berghofe 2003-10-29 Inserted additional checks in functions dest_prem and add_prod_factors, to allow side conditions of the form "x : S", where S is not an inductive set.
2003-10-29 paulson 2003-10-29 tidying
2003-10-29 berghofe 2003-10-29 Tuned proof of choice_eq.
2003-10-29 nipkow 2003-10-29 *** empty log message ***
2003-10-24 kleing 2003-10-24 added sydney unsw mirror. contact: me (gerwin.klein@nicta.com.au)
2003-10-22 paulson 2003-10-22 auto update
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions
2003-10-22 paulson 2003-10-22 recursion
2003-10-21 skalberg 2003-10-21 Added access to the mk_rews field (and friends).
2003-10-17 paulson 2003-10-17 Prevent recdef from looping when the inductio rule is simplified
2003-10-17 paulson 2003-10-17 improved tracing
2003-10-16 paulson 2003-10-16 partial conversion to Isar scripts
2003-10-16 paulson 2003-10-16 improved presentation
2003-10-16 paulson 2003-10-16 line-breaks; rewording
2003-10-16 paulson 2003-10-16 partial conversion to Isar scripts
2003-10-15 berghofe 2003-10-15 Fixed bug in mk_ind_def that caused the inductive definition package to crash in cases where the declaration of a constant and its definition were located in different theory files.
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 allow \<^sub> in identifiers
2003-10-15 kleing 2003-10-15 included \<^sub> in the range of identifier chars
2003-10-13 skalberg 2003-10-13 Fixed spelling error.
2003-10-10 berghofe 2003-10-10 Added overview page.
2003-10-10 berghofe 2003-10-10 Munich webserver is now atbroy1
2003-10-10 paulson 2003-10-10 trivial
2003-10-10 paulson 2003-10-10 finalconsts
2003-10-10 skalberg 2003-10-10 Made judgments automatically declared final.