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
2003-04-06 kleing 2003-04-06 run on sunbroy1, too
2003-04-06 nipkow 2003-04-06 *** empty log message ***
2003-04-05 nipkow 2003-04-05 Map.empty is now a translation
2003-04-05 kleing 2003-04-05 cleanup, mark old (<1994) deleted files as dead
2003-04-05 kleing 2003-04-05 cleanup, mark old (<1994) deleted files as dead
2003-04-05 kleing 2003-04-05 cleanup, mark old (<1994) deleted files as dead
2003-04-05 kleing 2003-04-05 cleanup, mark old (<1994) deleted files as dead
2003-04-05 kleing 2003-04-05 removed since 1994 or earlier
2003-04-04 berghofe 2003-04-04 Fixed bug in eta_long.
2003-04-04 berghofe 2003-04-04 type_of_G now applies type substitution before decomposing type.
2003-04-01 nipkow 2003-04-01 Made empty a translation rather than a constant.
2003-04-01 ballarin 2003-04-01 Fixed Coset.thy (proved theorem factorgroup_is_group).
2003-03-31 paulson 2003-03-31 more comments and tweaks
2003-03-31 paulson 2003-03-31 tidied
2003-03-29 berghofe 2003-03-29 Margin for pretty-printing is now a mutable reference.