src/HOL/NumberTheory/Fib.thy
2007-09-14 paulson 2007-09-14 tidied
2007-09-06 paulson 2007-09-06 new fun declaration
2007-07-10 haftmann 2007-07-10 expanded fragile proof
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 chaieb 2007-06-11 tuned Proof
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-31 webertj 2006-07-31 lin_arith_prover splits certain operators (e.g. min, max, abs)
2005-11-11 chaieb 2005-11-11 a proof step corrected due to the changement in the presburger method.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-25 paulson 2005-03-25 tidied up
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-15 wenzelm 2001-10-15 setsum syntax;
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2000-10-03 wenzelm 2000-10-03 tuned deps;
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization from HOL/ex