diff options
| author | mark | 2012-02-24 12:07:26 +0000 |
|---|---|---|
| committer | mark | 2012-02-24 12:07:26 +0000 |
| commit | cf0c3e813e4601f7462268703efd5b14424bd6c3 (patch) | |
| tree | 5ed504ddfb01b33857d9d235c35787e7f996fc54 /hol-light/TacticRecording/examples3.ml | |
| parent | 4ed83bcb88f220cc08c3223bd4f274eaa5f31e0c (diff) | |
Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.
Add wrapper function for :thm -> thm list.
Promote more objects.
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;; |