| Wed, 04 Mar 2009 17:12:23 -0800 | huffman | declare power_Suc [simp]; remove redundant type-specific versions of power_Suc | file | diff | annotate |
| Wed, 18 Feb 2009 19:32:26 -0800 | huffman | split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy | file | diff | annotate |