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.
2003-03-26 paulson 2003-03-26 Proofs for section 4.5.3
2003-03-25 berghofe 2003-03-25 Added show_brackets to settings menu.
2003-03-25 berghofe 2003-03-25 Re-structured some proofs in order to get rid of rule_format attribute.
2003-03-25 berghofe 2003-03-25 New theorems split_div' and mod_div_equality'.
2003-03-25 berghofe 2003-03-25 Presburger arithmetic
2003-03-25 berghofe 2003-03-25 Added examples for Presburger arithmetic.
2003-03-25 berghofe 2003-03-25 Added decision procedure for Presburger arithmetic.
2003-03-25 berghofe 2003-03-25 Added Presburger theory.
2003-03-25 berghofe 2003-03-25 Added hook for presburger arithmetic decision procedure.
2003-03-25 berghofe 2003-03-25 New decision procedure for Presburger arithmetic.
2003-03-23 nipkow 2003-03-23 *** empty log message ***
2003-03-21 paulson 2003-03-21 More on progress sets
2003-03-21 paulson 2003-03-21 quadratic reciprocity files
2003-03-20 paulson 2003-03-20 Gauss, UNITY, ZF
2003-03-20 paulson 2003-03-20 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
2003-03-18 paulson 2003-03-18 moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them to the new Group setup. Deleted Ring, Module from GroupTheory Minor UNITY changes
2003-03-18 nipkow 2003-03-18 toggled show_main_goal
2003-03-18 nipkow 2003-03-18 *** empty log message ***
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
2003-03-17 paulson 2003-03-17 More "progress set" material
2003-03-17 paulson 2003-03-17 moved one proof, added another
2003-03-14 ballarin 2003-03-14 Bugs fixed and operators finprod and finsum.
2003-03-14 kleing 2003-03-14 more about list_all2
2003-03-14 kleing 2003-03-14 fix for changes in HOL/Hoare/
2003-03-14 paulson 2003-03-14 Proved the main lemma on progress sets
2003-03-14 paulson 2003-03-14 new UN/INT simprules
2003-03-13 berghofe 2003-03-13 split_name no longer uses Sign.string_of_typ to encode types, since this depends on the print mode and may lead to unpredictable results.
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-03-11 berghofe 2003-03-11 addsplits / delsplits no longer ignore type of constant.
2003-03-10 ballarin 2003-03-10 First distributed version of Group and Ring theory.
2003-03-10 paulson 2003-03-10 New theory ProgressSets. Definition of closure sets
2003-03-10 paulson 2003-03-10 spelling
2003-03-06 paulson 2003-03-06 new UNITY examples theory
2003-03-06 paulson 2003-03-06 new logical equivalences
2003-03-06 paulson 2003-03-06 new simprule for int (nat n) and consequential changes
2003-03-06 kleing 2003-03-06 link to devel snapshot
2003-03-06 kleing 2003-03-06 obsolete