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.
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/