2000-05-05 nipkow 2000-05-05 Added AVL
2000-05-04 paulson 2000-05-04 if_weak_cong should make linear arithmetic faster
2000-05-04 paulson 2000-05-04 a safer way of proving literal equalities
2000-05-04 paulson 2000-05-04 from Suc...Suc to #m
2000-05-04 paulson 2000-05-04 of course it should use Main
2000-05-04 paulson 2000-05-04 new lemmas concerning powers and #mmm
2000-05-04 paulson 2000-05-04 changed 2 to #2
2000-05-04 paulson 2000-05-04 Suc 0 -> 1
2000-05-04 paulson 2000-05-04 card_Pow is no longer a default simprule because it uses unary 2
2000-05-04 paulson 2000-05-04 simprocs
2000-05-04 paulson 2000-05-04 further tidying of integer simprocs
2000-05-03 paulson 2000-05-03 removed obsolete simproc combine_coeff
2000-05-03 paulson 2000-05-03 Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int)
2000-05-03 paulson 2000-05-03 removed obsolete simprocs
2000-05-02 paulson 2000-05-02 removed obsolete "evenness" proofs
2000-05-02 paulson 2000-05-02 TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES
2000-05-02 paulson 2000-05-02 modified for new simprocs
2000-05-02 paulson 2000-05-02 now using binary naturals
2000-05-02 paulson 2000-05-02 various bug fixes
2000-05-02 paulson 2000-05-02 Cassini identity is easier to prove using INTEGERS
2000-05-02 paulson 2000-05-02 a more modern proof
2000-05-02 paulson 2000-05-02 now with combine_numerals
2000-05-02 paulson 2000-05-02 combine_numerals replaces both fold_Suc and combine_coeff
2000-05-02 paulson 2000-05-02 new simproc, replacing combine_coeffs and working for nat, int, real
2000-04-28 paulson 2000-04-28 signature change
2000-04-28 paulson 2000-04-28 inserted triviality check
2000-04-25 nipkow 2000-04-25 *** empty log message ***
2000-04-23 paulson 2000-04-23 new, but still slow, proofs using binary numerals
2000-04-23 paulson 2000-04-23 [Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
2000-04-23 paulson 2000-04-23 number_of now takes a type arg
2000-04-23 paulson 2000-04-23 this change saves 15 seconds
2000-04-23 paulson 2000-04-23 bug fixes to new simprocs
2000-04-23 paulson 2000-04-23 [Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
2000-04-23 paulson 2000-04-23 removed some duplication, etc.
2000-04-23 paulson 2000-04-23 now uses the new cancel_numerals simproc
2000-04-21 paulson 2000-04-21 Provers/Arith/inverse_fold.ML is already obsolete
2000-04-21 paulson 2000-04-21 cleaner exceptions
2000-04-21 paulson 2000-04-21 now works for coefficients, not just for numerals no longer works by subtraction, so no need for inverse_fold
2000-04-21 paulson 2000-04-21 new file containing simproc invocations, from NatBin.ML
2000-04-21 paulson 2000-04-21 moved the simproc code to NatSimprocs.ML
2000-04-21 paulson 2000-04-21 Provers/Arith/inverse_fold.ML is already obsolete
2000-04-21 paulson 2000-04-21 new file Integ/NatSimprocs.ML
2000-04-21 paulson 2000-04-21 Provers/Arith/inverse_fold.ML is already obsolete Integ/NatSimprocs.ML added
2000-04-20 nipkow 2000-04-20 *** empty log message ***
2000-04-19 nipkow 2000-04-19 *** empty log message ***
2000-04-19 wenzelm 2000-04-19 TuturialI;
2000-04-19 nipkow 2000-04-19 *** empty log message ***
2000-04-19 wenzelm 2000-04-19 check_file: keep expanded (!) absolute path;
2000-04-19 nipkow 2000-04-19 Adding generated files
2000-04-19 nipkow 2000-04-19 *** empty log message ***
2000-04-19 wenzelm 2000-04-19 fixed -c default value;
2000-04-19 nipkow 2000-04-19 Adding generated files.
2000-04-19 nipkow 2000-04-19 I wonder which files i forgot.
2000-04-19 nipkow 2000-04-19 *** empty log message ***
2000-04-19 nipkow 2000-04-19 I wonder if that's all?
2000-04-19 paulson 2000-04-19 deleted obsolete lemma_not_leI2
2000-04-19 paulson 2000-04-19 removal of less_SucI, le_SucI from default simpset
2000-04-18 paulson 2000-04-18 replaced obsolete diff_right_cancel by diff_diff_eq
2000-04-18 paulson 2000-04-18 added number_of_const: term
2000-04-18 paulson 2000-04-18 tidied