2003-05-05 paulson 2003-05-05 Complex, etc
2003-05-05 paulson 2003-05-05 deleted obsolete group formalization
2003-05-05 paulson 2003-05-05 New material on integration, etc. Moving Hyperreal/ex to directory Complex
2003-05-05 paulson 2003-05-05 new session Complex for the complex numbers
2003-05-05 paulson 2003-05-05 improved presentation of HOL/Auth theories
2003-05-05 kleing 2003-05-05 add mac test
2003-05-05 kleing 2003-05-05 fixed \<0>..\<9> (-> \<zero>..\<nine>)
2003-05-05 kleing 2003-05-05 document preparation tuning
2003-05-05 ballarin 2003-05-05 Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).
2003-05-03 kleing 2003-05-03 fix for new \isasymeuro
2003-05-02 ballarin 2003-05-02 File for document preparation.
2003-05-02 ballarin 2003-05-02 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
2003-05-02 kleing 2003-05-02 reduced package dependencies, use babel standard package for euro symbol
2003-05-02 kleing 2003-05-02 removed package marvosym (breaks \Rightarrow) reduced number of packages for "unusual symbols" replaced \textzerooldstyle by \mathbf{0} etc to get normal sized numbers
2003-05-02 kleing 2003-05-02 more documentation for packages in root.tex tuned IsaMakefile (make dependencies work)
2003-05-02 paulson 2003-05-02 moved Bij.thy from HOL/GroupTheory
2003-05-01 paulson 2003-05-01 new proofs about direct products, etc.
2003-05-01 paulson 2003-05-01 moving Bij.thy from GroupTheory to Algebra
2003-05-01 berghofe 2003-05-01 induct_impliesI is now unfolded.
2003-04-30 ballarin 2003-04-30 Unknown change.
2003-04-30 ballarin 2003-04-30 HOL-Algebra: New polynomial development added.
2003-04-30 ballarin 2003-04-30 HOL-Algebra: new dependencies.
2003-04-30 ballarin 2003-04-30 Simplifier: congruence rule update.
2003-04-30 nipkow 2003-04-30 added a thm
2003-04-30 ballarin 2003-04-30 Greatly extended CRing. Added Module.
2003-04-29 paulson 2003-04-29 tweaks
2003-04-29 paulson 2003-04-29 better guarantees
2003-04-28 kleing 2003-04-28 in \isanewline: \\ -> \par fixes "tex capacity exceeded" error for large theories
2003-04-28 ballarin 2003-04-28 Simplifier no longer aborts on failed congruence proof.
2003-04-28 berghofe 2003-04-28 Converted main proof to Isar.
2003-04-28 berghofe 2003-04-28 Converted main proofs to Isar.
2003-04-28 berghofe 2003-04-28 Added "break" flag to allow line breaks within \isa{...}
2003-04-27 berghofe 2003-04-27 Fixed problem in add_elim_realizer (concerning inductive predicates with parameters) introduced by last bugfix.
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2003-04-26 paulson 2003-04-26 catches exception DELETE
2003-04-25 kleing 2003-04-25 no need to be nice everywhere
2003-04-25 paulson 2003-04-25 Auth: certified email protocol
2003-04-25 paulson 2003-04-25 Changes required by the certified email protocol Public-key model now provides separate signature/encryption keys and also long-term symmetric keys.
2003-04-23 berghofe 2003-04-23 Fixed problem in add_elim_realizer which caused bound variables to get mixed up.
2003-04-23 kleing 2003-04-23 more documentation
2003-04-23 paulson 2003-04-23 Got rid of the [iff], which was effectively inserting converseD
2003-04-23 berghofe 2003-04-23 Tuned realizer for exE rule, to avoid blowup of extracted program.
2003-04-23 berghofe 2003-04-23 elim_vars now handles both Vars and Frees.
2003-04-23 berghofe 2003-04-23 elim_cong now eta-expands proofs on the fly if required.
2003-04-23 berghofe 2003-04-23 Eliminated most occurrences of rule_format attribute.
2003-04-16 nipkow 2003-04-16 header
2003-04-16 nipkow 2003-04-16 Added take/dropWhile thms
2003-04-15 kleing 2003-04-15 fixed document
2003-04-14 nipkow 2003-04-14 added thm"..." due to new Map.thy
2003-04-14 nipkow 2003-04-14 Added thms
2003-04-14 webertj 2003-04-14 Fixed non-escaped underscore in section headings (document generation should work again now).
2003-04-11 webertj 2003-04-11 Map.ML integrated into Map.thy
2003-04-09 paulson 2003-04-09 tidying
2003-04-09 paulson 2003-04-09 Removal of Summation theory
2003-04-08 berghofe 2003-04-08 Fixed bug in adjustcoeffeq_wp.
2003-04-08 berghofe 2003-04-08 try_param_tac now precomputes substitution for rule, in order to avoid problems with higher order unification.
2003-04-08 nipkow 2003-04-08 First working version
2003-04-07 nipkow 2003-04-07 added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
2003-04-06 kleing 2003-04-06 use 2 processors on sunbroy1