diff options
Diffstat (limited to 'hol-light/TacticRecording/examples3.ml')
| -rw-r--r-- | hol-light/TacticRecording/examples3.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml index 62a2ef70..f78ace3f 100644 --- a/hol-light/TacticRecording/examples3.ml +++ b/hol-light/TacticRecording/examples3.ml @@ -29,14 +29,14 @@ let LEMMA_1 = prove CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN HILABEL "induction" (INDUCT_TAC THEN - REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES]) THENL + REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL [HILABEL "base case" REAL_ARITH_TAC; ALL_TAC] THEN HILABEL "step case" (REWRITE_TAC[ARITH_RULE `1 <= SUC n`] THEN SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN REWRITE_TAC[real_pow; REAL_MUL_RID] THEN REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN - REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC));; + REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC)));; let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;; |