2013-03-26から1日間の記事一覧
# map(fun t-> MATCH_MP t (ARITH_RULE `~(5=0)`))[MOD_MOD_REFL; MOD_ADD_MO D; MOD_MULT_MOD2];; val it : thm list = [|- !m. m MOD 5 MOD 5 = m MOD 5; |- !a b. (a MOD 5 + b MOD 5) MOD 5 = (a + b) MOD 5; |- !m p. (m MOD 5 * p MOD 5) MOD 5 = (m *…