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