2011-12-05から1日間の記事一覧
SYM_CONV rewrites `a = b` to `b = a` # SYM_CONV `0=1`;; val it : thm = |- 0 = 1 1 = 0 # SYM (ARITH_RULE `0+1=1`);; val it : thm = |- 1 = 0 + 1 # SYM (ARITH_RULE `!m. m*0=0`);; Exception: Failure "dest_eq". CONV_RULE c th uses c to rewrite …