berghofe [Fri, 08 Jul 2005 11:57:15 +0200] rev 16765
Some changes to allow mutually recursive, overloaded functions with same name.
nipkow [Fri, 08 Jul 2005 11:39:59 +0200] rev 16764
added Davenport reference
nipkow [Fri, 08 Jul 2005 11:39:44 +0200] rev 16763
moved Davenport citation to Main, removed author list
nipkow [Fri, 08 Jul 2005 11:39:08 +0200] rev 16762
moved gcd to new GCD.thy
nipkow [Fri, 08 Jul 2005 11:38:53 +0200] rev 16761
proof needed updating because of arith
nipkow [Fri, 08 Jul 2005 11:38:30 +0200] rev 16760
changed imports due to new GCD.thy
nipkow [Fri, 08 Jul 2005 11:37:53 +0200] rev 16759
Used to be in Library/Primes
huffman [Fri, 08 Jul 2005 03:12:58 +0200] rev 16758
fix typo
huffman [Fri, 08 Jul 2005 03:09:32 +0200] rev 16757
replaced old continuity rules with new lemma cont2cont_lift_case
huffman [Fri, 08 Jul 2005 02:42:42 +0200] rev 16756
simplified proof of ifte_thms, removed ifte_simp