Lines Matching defs:REAL
744 val REAL = store_thm("REAL",
753 EXISTS_TAC ���&n��� THEN ASM_REWRITE_TAC[REAL] THEN
760 [REAL, REAL_LE_RADD, ZERO_LESS_EQ, LESS_EQ_MONO, REAL_LE_REFL] THEN
787 INDUCT_TAC THEN REWRITE_TAC[REAL, ADD, REAL_ADD_LID] THEN
794 INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO, MULT_CLAUSES, REAL,
856 REWRITE_TAC[REAL, REAL_LDISTRIB, REAL_MUL_RID, REAL_LT_ADDL] THEN
862 REWRITE_TAC[REAL, REAL_LDISTRIB, REAL_MUL_RID] THEN
892 GEN_TAC THEN REWRITE_TAC[num_CONV ���2:num���, REAL] THEN
1732 [REWRITE_TAC[REAL_LDISTRIB, REAL_RDISTRIB, REAL, REAL_MUL_LID] THEN
2246 REWRITE_TAC[ADD_CLAUSES, REAL, REAL_RDISTRIB] THEN BETA_TAC THEN
2256 DISCH_TAC THEN REWRITE_TAC[REAL, REAL_RDISTRIB] THEN