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:51:39 -0800 | huffman | move FrechetDeriv.thy to Library | file | diff | annotate | base |