2004-03-05 paulson 2004-03-05 tweaks
2004-03-05 paulson 2004-03-05 some new results
2004-03-05 paulson 2004-03-05 some new results
2004-03-05 paulson 2004-03-05 Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
2004-03-05 paulson 2004-03-05 patch to NumberTheory problems caused by Parity
2004-03-05 kleing 2004-03-05 do not remove heaps, used for afp test
2004-03-04 nipkow 2004-03-04 Lex: ML -> thy
2004-03-04 nipkow 2004-03-04 ML -> Isar
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-04 nipkow 2004-03-04 Removed ML files from Lex
2004-03-04 nipkow 2004-03-04 Conversion of ML files to Isar.
2004-03-03 schirmer 2004-03-03 added record_ex_sel_eq_simproc
2004-03-02 paulson 2004-03-02 fixed bugs in the setup of arithmetic procedures
2004-03-02 paulson 2004-03-02 converted Hyperreal/IntFloor to Isar script
2004-03-02 kleing 2004-03-02 tuned. proofs still gruesome..
2004-03-02 kleing 2004-03-02 converted MiniML to Isar
2004-03-02 kleing 2004-03-02 converted to Isar
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-03-01 paulson 2004-03-01 converted Hyperreal/HTranscendental to Isar script
2004-03-01 kleing 2004-03-01 converted to Isar
2004-03-01 kleing 2004-03-01 union/intersection over intervals
2004-02-29 berghofe 2004-02-29 Added specific code generator for number_of.
2004-02-26 paulson 2004-02-26 converted Hyperreal/Series to Isar script
2004-02-26 paulson 2004-02-26 converted Hyperreal/NatStar to Isar script
2004-02-26 nipkow 2004-02-26 corrected authors
2004-02-25 paulson 2004-02-25 converted Hyperreal/HSeries to Isar script
2004-02-25 berghofe 2004-02-25 find_tname now handles parameter renaming properly ("as they are printed").
2004-02-24 paulson 2004-02-24 converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
2004-02-24 paulson 2004-02-24 converted NSCA to Isar script
2004-02-23 paulson 2004-02-23 converted HOL/Complex/NSInduct to Isar script
2004-02-23 paulson 2004-02-23 converted HOL/Complex/NSCA to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CStar to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CSeries to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CLim to Isar script
2004-02-21 nipkow 2004-02-21 Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.
2004-02-20 paulson 2004-02-20 new "where" section
2004-02-20 nipkow 2004-02-20 moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
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