Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.

Add wrapper function for :thm -> thm list.
Promote more objects.

18 files changed, 470 insertions, 275 deletions

diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot
index fbe961bd..e96142f9 100644
--- a/hol-light/TacticRecording/ex.dot
+++ b/hol-light/TacticRecording/ex.dot
@@ -1,13 +1,24 @@
 digraph G {
-  subgraph cluster0 {
-    label = "process #1"
-    a0->a1->a2->a3
-  }
   subgraph cluster1 {
-    label = "process #2"
-    b0->b1->b2->b3
+    label = "induction";
+    517 -> 518;
+    517 -> 519;
+  }
+  subgraph cluster2 {
+    label = "base case";
+    528;
+  }
+  subgraph cluster3 {
+    label = "step case";
+    537 -> 538;
+    538 -> 540;
+    540 -> 542;
+    542 -> 544;
+    544 -> 546;
+    546 -> 548;
   }
-  b3->23
-  b2->a3
-  a3->23
+  512 -> 513;
+  513 -> 517;
+  518 -> 528;
+  519 -> 537;
 }
\ No newline at end of file
diff --git a/hol-light/TacticRecording/ex2.dot b/hol-light/TacticRecording/ex2.dot
new file mode 100644
index 00000000..fbe961bd
--- /dev/null
+++ b/hol-light/TacticRecording/ex2.dot
@@ -0,0 +1,13 @@
+digraph G {
+  subgraph cluster0 {
+    label = "process #1"
+    a0->a1->a2->a3
+  }
+  subgraph cluster1 {
+    label = "process #2"
+    b0->b1->b2->b3
+  }
+  b3->23
+  b2->a3
+  a3->23
+}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/ex3.dot b/hol-light/TacticRecording/ex3.dot
new file mode 100644
index 00000000..1704533d
--- /dev/null
+++ b/hol-light/TacticRecording/ex3.dot
@@ -0,0 +1,24 @@
+digraph G {
+  subgraph cluster1 {
+    label = "induction";
+    351 -> 352;
+    351 -> 353;
+    352 -> 358;
+    subgraph cluster2 {
+      label = "base case";
+      358;
+    }
+    353 -> 367;
+    subgraph cluster3 {
+      label = "step case";
+      367 -> 368;
+      368 -> 370;
+      370 -> 372;
+      372 -> 374;
+      374 -> 376;
+      376 -> 378;
+    }
+  }
+  344 -> 345;
+  345 -> 351;
+}
diff --git a/hol-light/TacticRecording/ex3.png b/hol-light/TacticRecording/ex3.png
new file mode 100644
index 00000000..f2edfbdc
--- /dev/null
+++ b/hol-light/TacticRecording/ex3.png
diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml
index fd0b446c..4e67ca18 100644
--- a/hol-light/TacticRecording/examples1.ml
+++ b/hol-light/TacticRecording/examples1.ml
@@ -43,8 +43,6 @@ g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
 e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
 let th = top_thm ();;
 
-#use"TacticRecording/mlexport.ml";;
-
 print_executed_proof true;;
 print_flat_proof true;;
 print_thenl_proof ();;
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;;
 
diff --git a/hol-light/TacticRecording/examples5.ml b/hol-light/TacticRecording/examples5.ml
index 6e34aaee..1ded99cf 100644
--- a/hol-light/TacticRecording/examples5.ml
+++ b/hol-light/TacticRecording/examples5.ml
@@ -1,79 +1,182 @@
-from Library/binomial.ml
+(* Taken from Library/prime.ml   *)
 
 prioritize_num();;
 
 (* ------------------------------------------------------------------------- *)
-(* Binomial coefficients.                                                    *)
+(* HOL88 compatibility (since all this is a port of old HOL88 stuff).        *)
 (* ------------------------------------------------------------------------- *)
 
-let binom = define
-  `(!n. binom(n,0) = 1) /\
-   (!k. binom(0,SUC(k)) = 0) /\
-   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
-
-let binom = theorem_wrap "binom" binom;;
-
-let BINOM_LT = prove
- (`!n k. n < k ==> (binom(n,k) = 0)`,
-  INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
-  ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;
-let BINOM_LT = theorem_wrap "BINOM_LT" BINOM_LT;;
-
-print_flat_proof true;;
-
-let BINOM_REFL = prove
- (`!n. binom(n,n) = 1`,
-  INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
-let BINOM_REFL = theorem_wrap "BINOM_REFL" BINOM_REFL;;
-
-let BINOM_1 = prove                
- (`!n. binom(n,1) = n`,
-  REWRITE_TAC[num_CONV `1`] THEN                                         
-  INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);;
-let BINOM_1 = theorem_wrap "BINOM_1" BINOM_1;;
-
-let BINOM_FACT = prove
- (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
-  INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
-  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
-  FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
-  REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;
-let BINOM_FACT = theorem_wrap "BINOM_FACT" BINOM_FACT;;
-
-let BINOM_EQ_0 = prove
- (`!n k. binom(n,k) = 0 <=> n < k`,
-  REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[BINOM_LT]] THEN
-  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
-  REWRITE_TAC[NOT_LT; LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
-  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
-  DISCH_TAC THEN MP_TAC(SYM(SPECL [`d:num`; `k:num`] BINOM_FACT)) THEN
-  ASM_REWRITE_TAC[GSYM LT_NZ; MULT_CLAUSES; FACT_LT]);;
-let BINOM_EQ_0 = theorem_wrap "BINOM_EQ_0" BINOM_EQ_0;;
-
-let BINOM_PENULT = prove
- (`!n. binom(SUC n,n) = SUC n`,
-  INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN
-  SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL
-   [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);;
-let BINOM_PENULT = theorem_wrap "BINOM_PENULT" BINOM_PENULT;;
+let MULT_MONO_EQ = prove
+ (`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`,
+  REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);;
 
+let LESS_ADD_1 = prove
+ (`!m n. n < m ==> (?p. m = n + (p + 1))`,
+  REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);;
+
+let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;;
+
+let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
+
+let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;;
+
+let LESS_EQ_0 = prove
+ (`!n. n <= 0 <=> (n = 0)`,
+  REWRITE_TAC[LE]);;
+
+let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;;
+
+let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;;
+
+let NOT_EXP_0 = prove
+ (`!m n. ~((SUC n) EXP m = 0)`,
+  REWRITE_TAC[EXP_EQ_0; NOT_SUC]);;
+
+let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;;
+
+let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;;
+
+let ZERO_LESS_EXP = prove
+ (`!m n. 0 < ((SUC n) EXP m)`,
+  REWRITE_TAC[LT_NZ; NOT_EXP_0]);;
+
+(* ------------------------------------------------------------------------- *)
+(* General arithmetic lemmas.                                                *)
 (* ------------------------------------------------------------------------- *)
-(* More potentially useful lemmas.                                           *)
+
+let MULT_FIX = prove(
+  `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`,
+  REPEAT GEN_TAC THEN
+  STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN
+  REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
+  REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN
+  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)     (* MMA: this is a problem !!!!)
+   [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
+  MATCH_ACCEPT_TAC MULT_MONO_EQ);;
+
+let LESS_EQ_MULT = prove(
+  `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`,
+  REPEAT GEN_TAC THEN
+  DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN
+  ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB;
+    GSYM ADD_ASSOC; LE_ADD]);;
+
+let LESS_MULT = prove(
+  `!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`,
+  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN
+   ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN
+  REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
+  REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN
+  ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN
+  MATCH_ACCEPT_TAC LESS_ADD_SUC);;
+
+let MULT_LCANCEL = prove(
+  `!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`,
+  REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN
+  REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);;
+
+let LT_POW2_REFL = prove
+ (`!n. n < 2 EXP n`,
+  INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);;
+
 (* ------------------------------------------------------------------------- *)
+(* Properties of the exponential function.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+let EXP_0 = prove
+ (`!n. 0 EXP (SUC n) = 0`,
+  REWRITE_TAC[EXP; MULT_CLAUSES]);;
+
+let EXP_MONO_LT_SUC = prove
+ (`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`,
+  REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);;
+
+let EXP_MONO_LE_SUC = prove
+ (`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`,
+  REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);;
+
+let EXP_MONO_EQ_SUC = prove
+ (`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`,
+  REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);;
+
+let EXP_EXP = prove
+ (`!x m n. (x EXP m) EXP n = x EXP (m * n)`,
+  REWRITE_TAC[EXP_MULT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere.            *)
+(* ------------------------------------------------------------------------- *)
+
+let DIFF_LEMMA = prove(
+  `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`,
+  REPEAT GEN_TAC THEN
+  DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN
+  DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
+  DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
+  GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN
+  REWRITE_TAC[ADD_ASSOC] THEN
+  REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);;
+
+let NOT_EVEN_EQ_ODD = prove(
+  `!m n. ~(2 * m = SUC(2 * n))`,
+  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
+  REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);;
+
+let CANCEL_TIMES2 = prove(
+  `!x y. (2 * x = 2 * y) <=> (x = y)`,
+  REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);;
+
+let EVEN_SQUARE = prove(
+  `!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`,
+  GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN
+  DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
+  EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN
+  REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN
+  REWRITE_TAC[MULT_AC]);;
+
+let ODD_SQUARE = prove(
+  `!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`,
+  GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
+  DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
+  ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
+  REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN
+  EXISTS_TAC `(m * m) + m` THEN
+  REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN
+  REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
+  REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
+  REWRITE_TAC[ADD_AC]);;
+
+let DIFF_SQUARE = prove(
+  `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`,
+  REPEAT GEN_TAC THEN
+  DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL
+   [SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL
+     [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[];
+      POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN
+      REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]];
+    POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
+    REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
+    REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
+    REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
+    AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN
+    AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);;
+
+let ADD_IMP_SUB = prove(
+  `!x y z. (x + y = z) ==> (x = z - y)`,
+  REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
+  REWRITE_TAC[ADD_SUB]);;
+
+let ADD_SUM_DIFF = prove(
+  `!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\
+                    ((w + v) + (w - v) = 2 * w)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
+  DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
+  REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
+  REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN
+  ONCE_REWRITE_TAC[ADD_SYM] THEN
+  REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);;
 
-let BINOM_TOP_STEP = prove
- (`!n k. ((n + 1) - k) * binom(n + 1,k) = (n + 1) * binom(n,k)`,
-  REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k:num` THENL
-   [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP
-     (ARITH_RULE `n < k ==> n + 1 = k \/ n + 1 < k`)) THEN
-    ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES];
-    ALL_TAC] THEN
-  FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN
-  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
-  REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN
-  MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN
-  MP_TAC(SPECL [`d:num`; `k:num`] BINOM_FACT) THEN
-  REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN
-  MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN
-  REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);;
-let BINOM_TOP_STEP = theorem_wrap "BINOM_TOP_STEP" BINOM_TOP_STEP;;
+let EXP_4 = prove(
+  `!n. n EXP 4 = (n EXP 2) EXP 2`,
+  GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
+  REWRITE_TAC[ARITH]);;
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml
index 370e0dc3..310ba677 100644
--- a/hol-light/TacticRecording/hiproofs.ml
+++ b/hol-light/TacticRecording/hiproofs.ml
@@ -143,7 +143,7 @@ let collapse_tensor h hs =
 let trivsimp_hiproof h =
   let trivsimp h =
      match h with
-       Hatomic (id,_) when (gtree_tactic (get_gtree id) = (Some "ALL_TAC",[]))
+       Hatomic (id,_) when (gtree_tactic (get_gtree id) = ("ALL_TAC",[]))
                                    -> Hidentity id
      | Hsequence (h1, Hempty)      -> h1
      | Hsequence (h1, Hidentity _) -> h1
@@ -161,7 +161,7 @@ let trivsimp_hiproof h =
   refactor_hiproof true trivsimp h;;
 
 
-(* Matching up lists of hiproofs *)
+(* Matching up two tensored lists to create single tensored list *)
 
 let rec matchup_hiproofs0 hs1 hs2 =
   match hs1 with
@@ -181,19 +181,17 @@ let matchup_hiproofs hs1 hs2 =
   map (fun (h1,hs2) -> Hsequence (h1, Htensor hs2)) hhs;;
 
 
-(* Separating out lists of hiproofs *)
+(* Separating out tensored list into head tensor and tail tensor  *)
 
-(*
 let separate_hiproofs0 h (hs01,hs02) =
   match h with
     Hsequence (h1,h2)
        -> (h1::hs01, h2::hs02)
   | _  -> let n = hiproof_arity h in
-          let h2 = Htensor (copy n Hidentity) in
+          let h2 = Htensor (copy n (Hidentity (-1))) in
           (h::hs01, h2::hs02);;
 
 let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
-*)
 
 
 (* Delabelling *)
@@ -205,7 +203,7 @@ let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
 let delabel_hiproof h =
   let delabel h =
      match h with
-       Hlabelled (Tactical (Some "SUBGOAL_THEN",_), h0)
+       Hlabelled (Tactical ("SUBGOAL_THEN",_), h0)
           -> h
      | Hlabelled (_,h0)
           -> h0
@@ -215,7 +213,7 @@ let delabel_hiproof h =
 let dethen_hiproof h =
   let dethen h =
      match h with
-       Hlabelled (Tactical (Some ("THEN" | "THENL"),_), h0)
+       Hlabelled (Tactical (("THEN" | "THENL"),_), h0)
           -> h0
      | _  -> h in
   refactor_hiproof true dethen h;;
@@ -248,32 +246,40 @@ let leftgroup_hiproof h =
      match h with
        Hsequence (h1, Hsequence (h2, h3))
           -> Hsequence (Hsequence (h1,h2), h3)
-(*     | Hsequence (h1, Htensor hs2)
-          -> if (exists is_hsequence hs2)
-               then let (hs2a,hs2b) = separate_hiproofs hs2 in
-                    Hsequence (Hsequence (h1, Htensor hs2a), Htensor hs2b)
-               else h  *)
      | _  -> h in
   refactor_hiproof true leftgroup h;;
 
 
 (* THEN insertion *)
 
-(* Looks for opportunities to use 'THEN' tacticals.  Note that this disrupts  *)
-(* arity consistency.                                                         *)
+(* Looks for opportunities to use 'THEN' tacticals.  Note that assumes a      *)
+(* normal form where trivsimp has taken place.                                *)
+
+let rec head_hiproof_equiv h1 h2 =
+  match (h1,h2) with
+    (Hatomic (id1,_), Hatomic (id2,_))
+       -> (gtree_tactic o get_gtree) id1 = (gtree_tactic o get_gtree) id2
+  | (Hidentity _, Hidentity _)
+       -> true
+  | (Hsequence (h1a,h1b), h2)
+       -> head_hiproof_equiv h1a h2
+  | (h1, Hsequence (h2a,h2b))
+       -> head_hiproof_equiv h1 h2a
+  | (Hempty, Hempty)
+       -> true
+  | _  -> false;;
 
 let thenise_hiproof h =
-  let thenise h =
+  let rec thenise h =
      match h with
        Hsequence (h1, Htensor (h2::h2s))
-          -> if (forall (fun h0 -> h0 = h2) h2s)
-               then Hlabelled (Tactical (Some "THEN", []), h)
-               else h
-     | Hsequence (h1, Hsequence (Htensor (h2::h2s), h3))
-          -> if (forall (fun h0 -> h0 = h2) h2s)
-               then Hsequence
-                     (Hlabelled (Tactical (Some "THEN", []),
-                                 Hsequence (h1, Htensor (h2::h2s))), h3)
+          -> if not (is_hidentity h2) & (forall (head_hiproof_equiv h2) h2s) 
+               then let (hs2a,hs2b) = separate_hiproofs (h2::h2s) in
+                    let h' = Hsequence
+                               (Hlabelled (Tactical ("THEN",[]),
+                                           Hsequence (h1, Htensor hs2a)),
+                                Htensor hs2b) in
+                    thenise h'
                else h
      | _  -> h in
   refactor_hiproof false thenise h;;
@@ -360,10 +366,7 @@ let rec hiproof_graph0 h =
 let hiproof_graph h =
   let ges = hiproof_graph0 h in
   let ids = graph_nodes ges in
-  let tacname_of_id id =
-     match ((fst o gtree_tactic1 o get_gtree) id) with
-       Some x -> x
-     | None   -> "<tactic>" in
+  let tacname_of_id id = (fst o gtree_tactic1 o get_gtree) id in
   let ges' = map (fun id -> Name (id, tacname_of_id id)) ids in
   ges' @ ges;;
 
diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml
index b1309f84..5de28331 100644
--- a/hol-light/TacticRecording/lib.ml
+++ b/hol-light/TacticRecording/lib.ml
@@ -19,6 +19,15 @@ let rec foldr f xs a =
   | []      -> a;;
 
 
+(* foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a                                 *)
+
+let rec foldr1 f xs =
+  match xs with
+    x::[]   -> x
+  | x1::xs2 -> f x1 (foldr1 f xs2)
+  | []      -> failwith "foldr1: Empty list";;
+
+
 (* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b                            *)
 
 let rec foldl f a xs =
diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml
index bfdc1488..57c82547 100644
--- a/hol-light/TacticRecording/main.ml
+++ b/hol-light/TacticRecording/main.ml
@@ -6,6 +6,7 @@
 
 (* Datatypes and recording mechanism *)
 
+#use "TacticRecording/mldata.ml";;
 #use "TacticRecording/xthm.ml";;
 #use "TacticRecording/xtactics.ml";;
 #use "TacticRecording/tacticrec.ml";;
diff --git a/hol-light/TacticRecording/mldata.ml b/hol-light/TacticRecording/mldata.ml
new file mode 100644
index 00000000..b547a89b
--- /dev/null
+++ b/hol-light/TacticRecording/mldata.ml
@@ -0,0 +1,33 @@
+
+
+type mlarg =
+   Mlint of int
+ | Mlstring of string
+ | Mlterm of term
+ | Mltype of hol_type
+ | Mlthm of mldata
+ | Mlpair of mlarg * mlarg
+ | Mllist of mlarg list
+ | Mlfn of mldata
+
+and mldata = string * mlarg list;;          (* ML object name and args *)
+
+
+type label =
+   Tactical of mldata
+ | Label of string;;
+
+
+(* Atomic tests *)
+
+let is_atomic_mlarg arg =
+  match arg with
+    Mlthm (_,(_::_)) | Mlpair _ | Mlfn (_, _::_) -> false
+  | _ -> true;;
+
+let is_atomic_mldata ((x,args):mldata) = (is_empty args);;
+
+
+(* active_info *)
+
+let active_info = ("...",[]);;
diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml
index 429cb770..9a9207d5 100644
--- a/hol-light/TacticRecording/mlexport.ml
+++ b/hol-light/TacticRecording/mlexport.ml
@@ -15,10 +15,9 @@
 (* ** UTILS ** *)
 
 
-(* Printer for tactic 'finfo' *)
+(* Printer for tactic is just the ML data printer *)
 
-let print_tactic br ((x_,args):finfo) =
-  print_finfo "<tactic>" br ((x_,args):finfo);;
+let print_tactic br obj = print_mldata br obj;;
 
 
 (* Printer for subgoal comments *)
@@ -35,8 +34,8 @@ let print_hicomment_line ns =
 let print_tactic_line_with pr arg =
   (print_string "e ("; pr false arg; print_string ");;\n");;
 
-let print_tactic_line info =
-  (print_tactic_line_with print_tactic info);;
+let print_tactic_line obj =
+  (print_tactic_line_with print_tactic obj);;
 
 let print_hitrace_line_with fl pr htr =
   match htr with
@@ -91,22 +90,22 @@ let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;;
 
 let rec print_hiproof2 br h =
   match h with
-    Hlabelled (Tactical (Some "REPEAT", _), Hsequence (h1,h2)) (* if repeated *)
+    Hlabelled (Tactical ("REPEAT", _), Hsequence (h1,h2)) (* if repeated *)
        -> (print_string_if br "(";
            print_string "REPEAT ";
            print_hiproof2 true h1;
            print_string_if br ")")
-  | Hlabelled (Tactical (Some "THEN", _),                     (* if tac2 used *)
+  | Hlabelled (Tactical ("THEN", _),                     (* if tac2 used *)
                Hsequence (h1, Htensor (h2::h2s)))
        -> (print_string_if br "(";
            print_hiproof2 false h1;
            print_string " THEN ";
            print_hiproof2 true h2;
            print_string_if br ")")
-  | Hlabelled (Tactical ((Some "SUBGOAL_THEN",                (* special case *)
-                         (Fterm tm)::[farg]) as info),
+  | Hlabelled (Tactical (("SUBGOAL_THEN",                (* special case *)
+                         (Mlterm tm)::[_]) as obj),
                _)
-       -> (print_tactic br info)
+       -> (print_tactic br obj)
   | Hlabelled (Label x, h)
        -> (print_string_if br "(";
            print_string "HILABEL ";
@@ -145,7 +144,8 @@ let print_executed_proof fl = print_gtree_executed_proof fl !the_goal_tree;;
 (* ! 'REPEAT' not currently catered for.                                      *)
 
 let print_hiproof_packaged_proof h =
-  let h' = (thenise_hiproof o trivsimp_hiproof o leftgroup_hiproof) h in
+  let h' = (trivsimp_hiproof o thenise_hiproof o
+            trivsimp_hiproof o leftgroup_hiproof) h in
   print_tactic_line_with print_hiproof2 h';;
 
 let print_gtree_packaged_proof gtr =
diff --git a/hol-light/TacticRecording/printutils.ml b/hol-light/TacticRecording/printutils.ml
index 9131e18d..aa74ee22 100644
--- a/hol-light/TacticRecording/printutils.ml
+++ b/hol-light/TacticRecording/printutils.ml
@@ -22,34 +22,35 @@ let print_goalid id = print_int id;;
 let print_indent d = print_string (String.make d ' ');;
 
 
-(* Printer for 'finfo' *)
+(* Printer for 'mldata' *)
 
-let rec print_farg x0 br arg =
+let rec print_mlarg br arg =
   match arg with
-    Fint n       -> print_int n
-  | Fstring x    -> print_fstring x
-  | Fterm tm     -> print_fterm tm
-  | Ftype ty     -> print_ftype ty
-  | Fthm prf     -> print_finfo "<rule>" br prf
-  | Fpair (arg1,arg2)
-       -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in
+    Mlint n       -> print_int n
+  | Mlstring x    -> print_fstring x
+  | Mlterm tm     -> print_fterm tm
+  | Mltype ty     -> print_ftype ty
+  | Mlthm prf     -> print_mldata br prf
+  | Mlpair (arg1,arg2)
+       -> let sep =
+             if (forall is_atomic_mlarg [arg1;arg2]) then "," else ", " in
           (print_string_if br "(";
-           print_farg x0 false arg1;
+           print_mlarg false arg1;
            print_string sep;
-           print_farg x0 false arg2;
+           print_mlarg false arg2;
            print_string_if br ")")
-  | Flist args 
-       -> let sep = if (forall is_atomic_farg args) then ";" else "; " in
+  | Mllist args 
+       -> let sep = if (forall is_atomic_mlarg args) then ";" else "; " in
           (print_string "[";
-           print_seplist (print_farg x0 false) sep args;
+           print_seplist (print_mlarg false) sep args;
            print_string "]")
-  | Ffn f
-       -> (print_finfo x0 br f)
+  | Mlfn f
+       -> (print_mldata br f)
 
-and print_finfo x0 br ((x_,args):finfo) =
+and print_mldata br ((x,args):mldata) =
   (print_string_if (br & not (is_empty args)) "(";
-   print_option x0 x_;
-   do_list (fun arg -> print_string " "; print_farg x0 true arg) args;
+   print_string x;
+   do_list (fun arg -> print_string " "; print_mlarg true arg) args;
    print_string_if (br & not (is_empty args)) ")");;
 
 
@@ -57,5 +58,4 @@ and print_finfo x0 br ((x_,args):finfo) =
 
 let print_label l =
   match l with
-    Tactical (Some x, _) | Label x  -> print_fstring x
-  | Tactical (None, _)              -> print_fstring "<tactical>";;
+    Tactical (x,_) | Label x  -> print_fstring x;;
diff --git a/hol-light/TacticRecording/promote.ml b/hol-light/TacticRecording/promote.ml
index cd711707..c19abb8a 100644
--- a/hol-light/TacticRecording/promote.ml
+++ b/hol-light/TacticRecording/promote.ml
@@ -252,11 +252,15 @@ let BINDER_CONV = conv_conv_wrap "BINDER_CONV" BINDER_CONV;;
 let SUB_CONV = conv_conv_wrap "SUB_CONV" SUB_CONV;;
 let BINOP_CONV = conv_conv_wrap "BINOP_CONV" BINOP_CONV;;
 let GSYM = rule_wrap "GSYM" GSYM;;
+let CONJUNCTS = multirule_wrap "CONJUNCTS" CONJUNCTS;;
+let SPEC_ALL = rule_wrap "SPEC_ALL" SPEC_ALL;;
 let ISPECL = termlist_rule_wrap "ISPECL" ISPECL;;
 let ALL_CONV = conv_wrap "ALL_CONV" ALL_CONV;;
 let (REPEATC) = conv_conv_wrap "REPEATC" REPEATC;;
 let ONCE_DEPTH_CONV = conv_conv_wrap "ONCE_DEPTH_CONV" ONCE_DEPTH_CONV;;
 
+let REWRITE_RULE = thmlist_rule_wrap "REWRITE_RULE" REWRITE_RULE;;
+
 let num_CONV = conv_wrap "num_CONV" num_CONV;;
 let ARITH_RULE = conv_wrap "ARITH_RULE" ARITH_RULE;;
 
@@ -272,14 +276,24 @@ let EQ_IMP = theorem_wrap "EQ_IMP" EQ_IMP;;
 
 let ARITH = theorem_wrap "ARITH" ARITH;;
 let ARITH_EQ = theorem_wrap "ARITH_EQ" ARITH_EQ;;
+let ADD_ASSOC = theorem_wrap "ADD_ASSOC" ADD_ASSOC;;
 let ADD_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;;
+let LEFT_ADD_DISTRIB = theorem_wrap "LEFT_ADD_DISTRIB" LEFT_ADD_DISTRIB;;
+let RIGHT_ADD_DISTRIB = theorem_wrap "RIGHT_ADD_DISTRIB" RIGHT_ADD_DISTRIB;;
 let MULT_CLAUSES =theorem_wrap "MULT_CLAUSES" MULT_CLAUSES;;
 let SUB_REFL = theorem_wrap "SUB_REFL" SUB_REFL;;
 let ADD1 =  theorem_wrap "ADD1" ADD1;;
+let EQ_MULT_LCANCEL = theorem_wrap "EQ_MULT_LCANCEL" EQ_MULT_LCANCEL;;
+let LE_EXISTS = theorem_wrap "LE_EXISTS" LE_EXISTS;;
+let LE_ADD = theorem_wrap "LE_ADD" LE_ADD;;
 let LE_1 = theorem_wrap "LE_1" LE_1;;
 let LE_REFL = theorem_wrap "LE_REFL" LE_REFL;;
 let LT_SUC = theorem_wrap "LT_SUC" LT_SUC;;
+let LT_EXISTS = theorem_wrap "LT_EXISTS" LT_EXISTS;;
+let LT_NZ = theorem_wrap "LT_NZ" LT_NZ;;
+let EXP_EQ_0 = theorem_wrap "EXP_EQ_0" EXP_EQ_0;;
 let FACT = theorem_wrap "FACT" FACT;;
+let  = theorem_wrap "" ;;
 
 let REAL_ADD_LDISTRIB = theorem_wrap "REAL_ADD_LDISTRIB" REAL_ADD_LDISTRIB;;
 let REAL_OF_NUM_ADD = theorem_wrap "REAL_OF_NUM_ADD" REAL_OF_NUM_ADD;;
diff --git a/hol-light/TacticRecording/tacticrec.ml b/hol-light/TacticRecording/tacticrec.ml
index 7df77fad..c65ee71c 100644
--- a/hol-light/TacticRecording/tacticrec.ml
+++ b/hol-light/TacticRecording/tacticrec.ml
@@ -60,7 +60,7 @@ type ginfo =
  * unit option ref;;                 (* Formal proof (optional) *)
 
 type gstep =
-   Gatom of finfo                    (* Atomic tactic *)
+   Gatom of mldata                   (* Atomic tactic *)
  | Gbox of (label * gtree * bool)    (* Box for a tactical; flag for special *)
 
 and gtree0 =
@@ -80,19 +80,19 @@ and gtree =
 (*                                                                            *)
 (*  (_, ref                                                                   *)
 (*   Gexecuted                                                                *)
-(*     (Gbox (Tactical (Some "T1"))                                           *)
+(*     (Gbox (Tactical ("T1",[])                                              *)
 (*        (_, ref                                                             *)
 (*         Gexecuted                                                          *)
-(*           (Gatom (Some "T2"),                                              *)
-(*            [ (_, ref Gexecuted (Gatom (Some "WF"), []));                   *)
+(*           (Gatom ("T2",[]),                                                *)
+(*            [ (_, ref Gexecuted (Gatom ("WF",[]), []));                     *)
 (*              (_, ref Gexit _) ])),                                         *)
 (*      [ (_, ref                                                             *)
 (*         Gexecuted                                                          *)
-(*           (Gbox (Tactical (Some "DP"))                                     *)
+(*           (Gbox (Tactical ("DP",[]))                                       *)
 (*              (_, ref                                                       *)
 (*               Gexecuted                                                    *)
-(*                 (Gatom (Some "Normalise"),                                 *)
-(*                  [ (_, ref Gexecuted (Gatom (Some "Taut"), [])) ])),       *)
+(*                 (Gatom ("Normalise",[]),                                   *)
+(*                  [ (_, ref Gexecuted (Gatom ("Taut",[]), [])) ])),         *)
 (*            [])) ]))                                                        *)
 
 
@@ -125,7 +125,7 @@ let gtree_fproof ((info,_):gtree) = ginfo_fproof info;;
 
 let gstep_tactic (gstp:gstep) =
   match gstp with
-    Gatom info | Gbox (Tactical info, _, true) -> info
+    Gatom obj | Gbox (Tactical obj, _, true) -> obj
   | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";;
 
 let gtree_proof ((_,gtrm):gtree) =
@@ -304,9 +304,11 @@ let (xTAC_PROOF : goal * xtactic -> thm) =
 let xprove(t,tac) =
   let th = xTAC_PROOF(([],t),tac) in
   let t' = concl th in
-  if t' = t then th else
-  try EQ_MP (ALPHA t' t) th
-  with Failure _ -> failwith "prove: justification generated wrong theorem";;
+  let th' =
+    if t' = t then th else
+    try EQ_MP (ALPHA t' t) th
+    with Failure _ -> failwith "prove: justification generated wrong theorem" in
+  mk_xthm (th', ("<tactic-proof>",[]))
 
 let xset_goal(asl,w) =
   current_xgoalstack :=
diff --git a/hol-light/TacticRecording/wrappers.ml b/hol-light/TacticRecording/wrappers.ml
index 1244c89f..115163d4 100644
--- a/hol-light/TacticRecording/wrappers.ml
+++ b/hol-light/TacticRecording/wrappers.ml
@@ -11,19 +11,19 @@
 (* ** THEOREM-RELATED WRAPPER FUNCTIONS ** *)
 
 
-(* finfo_as_meta_arg *)
+(* mldata_as_meta_arg *)
 
-let finfo_as_meta_arg (info:finfo) =
-  match info with
-    (x_, ((_::_) as args))
-       -> Ffn (x_, front args)
-  | _  -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";;
+let mldata_as_meta_arg (obj:mldata) =
+  match obj with
+    (x, ((_::_) as args))
+       -> Mlfn (x, front args)
+  | _  -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";;
 
-let finfo_as_meta2_arg (info:finfo) =
-  match info with
-    (x_, ((_::_) as args))
-       -> Ffn (x_, (front o front) args)
-  | _  -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";;
+let mldata_as_meta2_arg (obj:mldata) =
+  match obj with
+    (x, ((_::_) as args))
+       -> Mlfn (x, (front o front) args)
+  | _  -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";;
 
 
 (* detect_rule_app *)
@@ -34,24 +34,24 @@ let finfo_as_meta2_arg (info:finfo) =
 (* result is returned along with an 'farg' that captures the rule.            *)
 
 let detect_rule_app (mfunc:('a->thm)->'b) (xr:'a->xthm) : 'c =
-  let temp = ref (Ffn (Some "<rule>", []) : farg) in
+  let temp = ref (Mlfn ("<rule>", []) : mlarg) in
   let r arg = let xth = xr arg in
-              let (th,info) = dest_xthm xth in
-              (temp := finfo_as_meta_arg info;
+              let (th,obj) = dest_xthm xth in
+              (temp := mldata_as_meta_arg obj;
                th) in
   let th = mfunc r in
   (th,!temp);;
 
 let detect_metarule_app (mfunc:(('a->thm)->'b->thm)->'c)
                         (xmr:('a->xthm)->'b->xthm) : 'd =
-  let temp = ref (Ffn (Some "<meta-rule>", []) : farg) in
+  let temp = ref (Mlfn ("<meta-rule>",[]) : mlarg) in
   let mr marg arg = let xmarg arg0 =
                        let th = marg arg0 in
-                       let info = (Some "<rule>", [Ffn (Some "<arg>",[])]) in
-                       mk_xthm (th,info) in
+                       let obj = ("<rule>", [Mlfn ("<arg>",[])]) in
+                       mk_xthm (th,obj) in
                     let xth = xmr xmarg arg in
-                    let (th,info) = dest_xthm xth in
-                    (temp := finfo_as_meta2_arg info;
+                    let (th,obj) = dest_xthm xth in
+                    (temp := mldata_as_meta2_arg obj;
                      th) in
   let th = mfunc mr in
   (th,!temp);;
@@ -60,7 +60,7 @@ let detect_metarule_app (mfunc:(('a->thm)->'b->thm)->'c)
 (* Theorem wrapper *)
 
 let theorem_wrap (x:string) (th:thm) : xthm =
-  (th, (Some x, []));;
+  (th, (x,[]));;
 
 
 (* Rule wrappers *)
@@ -68,94 +68,109 @@ let theorem_wrap (x:string) (th:thm) : xthm =
 (* Lots of rule wrappers are required because there are many different type   *)
 (* shapes for rules.                                                          *)
 
-let rule_wrap0 finfo (r:'a->thm) (arg:'a) : xthm =
+let rule_wrap0 obj (r:'a->thm) (arg:'a) : xthm =
   let th' = r arg in
-  mk_xthm (th',finfo);;
+  mk_xthm (th',obj);;
 
 let conv_wrap x (r:term->thm) (tm:term) : xthm =
-  rule_wrap0 (Some x, [Fterm tm]) r tm;;
+  rule_wrap0 (x, [Mlterm tm]) r tm;;
 
 let thm_conv_wrap x (r:thm->term->thm) (xth:xthm) tm : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;;
+  rule_wrap0 (x, [Mlthm prf; Mlterm tm]) (r th) tm;;
 
 let thmlist_conv_wrap x (r:thm list->term->thm) xths (tm:term) : xthm =
   let (ths,prfs) = unzip (map dest_xthm xths) in
-  rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm])
+  rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlterm tm])
              (r ths) tm;;
 
 let rule_wrap x (r:thm->thm) (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Fthm prf]) r th;;
+  rule_wrap0 (x, [Mlthm prf]) r th;;
 
 let drule_wrap x (r:thm->thm->thm) (xth1:xthm) (xth2:xthm) : xthm =
   let (th1,prf1) = dest_xthm xth1 in
   let (th2,prf2) = dest_xthm xth2 in
-  rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;;
+  rule_wrap0 (x, [Mlthm prf1; Mlthm prf2]) (r th1) th2;;
 
 let prule_wrap x (r:thm*thm->thm) ((xth1:xthm),(xth2:xthm)) : xthm =
   let (th1,prf1) = dest_xthm xth1 in
   let (th2,prf2) = dest_xthm xth2 in
-  rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);;
+  rule_wrap0 (x, [Mlpair(Mlthm prf1, Mlthm prf2)]) r (th1,th2);;
 
 let trule_wrap x (r:thm->thm->thm->thm)
                  (xth1:xthm) (xth2:xthm) (xth3:xthm) : xthm =
   let (th1,prf1) = dest_xthm xth1 in
   let (th2,prf2) = dest_xthm xth2 in
   let (th3,prf3) = dest_xthm xth3 in
-  rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;;
+  rule_wrap0 (x, [Mlthm prf1; Mlthm prf2; Mlthm prf3]) (r th1 th2) th3;;
 
 let term_rule_wrap x (r:term->thm->thm) tm (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;;
+  rule_wrap0 (x, [Mlterm tm; Mlthm prf]) (r tm) th;;
 
 let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;;
+  rule_wrap0 (x, [Mlpair(Mlterm tm1,Mlterm tm2); Mlthm prf]) (r (tm1,tm2)) th;;
 
 let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,xth0) (xth:xthm) : xthm =
   let (th0,prf0) = dest_xthm xth0 in
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;;
+  rule_wrap0 (x, [Mlpair(Mlterm tm, Mlthm prf0); Mlthm prf]) (r (tm,th0)) th;;
 
 let termlist_rule_wrap x (r:term list->thm->thm) tms (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf])
+  rule_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms); Mlthm prf])
              (r tms) th;;
 
 let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x,
-              [Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta);
-               Fthm prf])
+  rule_wrap0 (x,
+              [Mllist (map (fun (tm1,tm2) -> Mlpair(Mlterm tm1, Mlterm tm2))
+                           theta);
+               Mlthm prf])
              (r theta) th;;
 
 let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm)
                          theta (xth:xthm) : xthm =
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x,
-              [Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta);
-               Fthm prf])
+  rule_wrap0 (x,
+              [Mllist (map (fun (tm1,tm2) -> Mlpair(Mltype tm1, Mltype tm2))
+                           theta);
+               Mlthm prf])
              (r theta) th;;
 
 let thmlist_rule_wrap x (r:thm list->thm->thm) xths (xth:xthm) : xthm =
   let (ths,prfs) = unzip (map dest_xthm xths) in
   let (th,prf) = dest_xthm xth in
-  rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf])
+  rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlthm prf])
              (r ths) th;;
 
 
+(* Multi-rule wrappers *)
+
+let multirule_wrap0 obj (r:'a->thm list) (arg:'a) : xthm list =
+  let ths' = r arg in
+  let n = length ths' in
+  let infos' = map (fun i -> ("el", [Mlint i; Mlfn obj])) (0 -- (n-1)) in
+  map mk_xthm (zip ths' infos');; 
+
+let multirule_wrap x (r:thm->thm list) (xth:xthm) : xthm list =
+  let (th,prf) = dest_xthm xth in
+  multirule_wrap0 (x, [Mlthm prf]) r th;;
+
+
 (* Meta rule wrappers *)
 
 let meta_rule_wrap0 info0 (mr:('a->thm)->'b->thm)
                           (xr:'a->xthm) (arg:'b) : xthm =
   let (th',f) = detect_rule_app (fun r -> mr r arg) xr in
-  let (x_,args0) = info0 in
-  let info' = (x_, f::args0) in
-  (th',info');;
+  let (x,args0) = info0 in
+  let obj' = (x, f::args0) in
+  (th',obj');;
 
 let conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm =
-  meta_rule_wrap0 (Some x, [Fterm tm]) mc xc tm;;
+  meta_rule_wrap0 (x, [Mlterm tm]) mc xc tm;;
 
 
 
@@ -171,10 +186,10 @@ let conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm =
 (* returns 'goalstate', but that also returns a 'gstep' summary of the        *)
 (* operation.  This is used to promote every basic tactic-based function.     *)
 
-let infotactic_wrap (infotac:goal->goalstate*finfo) (xg:xgoal) : xgoalstate =
+let infotactic_wrap (infotac:goal->goalstate*mldata) (xg:xgoal) : xgoalstate =
   let (g,id) = dest_xgoal xg in
-  let ((meta,gs,just),info) = infotac g in
-  let xgs = extend_gtree id (Gatom info) gs in
+  let ((meta,gs,just),obj) = infotac g in
+  let xgs = extend_gtree id (Gatom obj) gs in
   (meta,xgs,just);;
 
 
@@ -203,36 +218,36 @@ let infobox_wrap (xinfotac:xgoal->xgoalstate*label) (xg:xgoal) : xgoalstate =
 (* This is for wrapping around a tactic, to promote it to work on xgoals and  *)
 (* incorporate the results into an existing gtree.                            *)
 
-let tactic_wrap0 info (tac:tactic) : xtactic =
-  let infotac g = (tac g, info) in
+let tactic_wrap0 obj (tac:tactic) : xtactic =
+  let infotac g = (tac g, obj) in
   infotactic_wrap infotac;;
 
 let tactic_wrap x tac =
-  tactic_wrap0 (Some x, []) tac;;
+  tactic_wrap0 (x, []) tac;;
 
 let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic =
-  tactic_wrap0 (Some x, [Fstring s]) (tac s);;
+  tactic_wrap0 (x, [Mlstring s]) (tac s);;
 
 let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic =
-  tactic_wrap0 (Some x, [Fterm tm]) (tac tm);;
+  tactic_wrap0 (x, [Mlterm tm]) (tac tm);;
 
 let termpair_tactic_wrap x (tac:term*term->tactic) (tm1,tm2) : xtactic =
-  tactic_wrap0 (Some x, [Fpair (Fterm tm1, Fterm tm2)]) (tac (tm1,tm2));;
+  tactic_wrap0 (x, [Mlpair (Mlterm tm1, Mlterm tm2)]) (tac (tm1,tm2));;
 
 let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic =
-  tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms)]) (tac tms);;
+  tactic_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms)]) (tac tms);;
 
 let thm_tactic_wrap x (tac:thm->tactic) (xth:xthm) : xtactic =
   let (th,prf) = dest_xthm xth in
-  tactic_wrap0 (Some x, [Fthm prf]) (tac th);;
+  tactic_wrap0 (x, [Mlthm prf]) (tac th);;
 
 let thmlist_tactic_wrap x (tac:thm list->tactic) (xths:xthm list) : xtactic =
   let (ths,prfs) = unzip (map dest_xthm xths) in
-  tactic_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs)]) (tac ths);;
+  tactic_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs)]) (tac ths);;
 
 let stringthm_tactic_wrap x (tac:string->thm->tactic) s (xth:xthm) : xtactic =
   let (th,prf) = dest_xthm xth in
-  tactic_wrap0 (Some x, [Fstring s; Fthm prf]) (tac s th);;
+  tactic_wrap0 (x, [Mlstring s; Mlthm prf]) (tac s th);;
 
 
 (* Meta-tactic wrapper *)
@@ -243,27 +258,27 @@ let meta_tactic_wrap0 info0 (mtac:('a->thm)->tactic)
                             (xr:'a->xthm) : xtactic =
   let infotac g =
      let (gst,f) = detect_rule_app (fun r -> mtac r g) xr in
-     let (x_,args0) = info0 in
-     let info = (x_, f::args0) in
-     (gst,info) in
+     let (x,args0) = info0 in
+     let obj = (x, f::args0) in
+     (gst,obj) in
   infotactic_wrap infotac;;
 
 let conv_tactic_wrap x (mtac:conv->tactic) (xc:xconv) : xtactic =
-  meta_tactic_wrap0 (Some x, []) mtac xc;;
+  meta_tactic_wrap0 (x, []) mtac xc;;
 
 let metameta_tactic_wrap info0 (mmtac:(('a->thm)->'b->thm)->tactic)
                                (xmr:('a->xthm)->'b->xthm) : xtactic =
   let infotac g =
      let (gst,f) = detect_metarule_app (fun mr -> mmtac mr g) xmr in
-     let (x_,args0) = info0 in
-     let info = (x_, f::args0) in
-     (gst,info) in
+     let (x,args0) = info0 in
+     let obj = (x, f::args0) in
+     (gst,obj) in
   infotactic_wrap infotac;;
 
 let convconvthmlist_tactic_wrap x (mmtac:(conv->conv)->thm list->tactic)
                                  (xmc:xconv->xconv) (xths:xthm list) : xtactic =
   let (ths,prfs) = unzip (map dest_xthm xths) in
-  metameta_tactic_wrap (Some x, [Flist (map (fun prf -> Fthm prf) prfs)])
+  metameta_tactic_wrap (x, [Mllist (map (fun prf -> Mlthm prf) prfs)])
                        (fun mc -> mmtac mc ths)
                        xmc;;
 
@@ -277,22 +292,22 @@ let convconvthmlist_tactic_wrap x (mmtac:(conv->conv)->thm list->tactic)
 (* already be promoted to work with xtactics and xgoals.  This must done by   *)
 (* hand for each tactical by trivially adjusting its original source code.    *)
 
-let tactical_wrap0 info (xttcl:'a->xtactic) (arg:'a) : xtactic =
-  let xinfotac xg = (xttcl arg xg, Tactical info) in
+let tactical_wrap0 obj (xttcl:'a->xtactic) (arg:'a) : xtactic =
+  let xinfotac xg = (xttcl arg xg, Tactical obj) in
   infobox_wrap xinfotac;;
 
 let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic =
-  tactical_wrap0 (Some x, []) xttcl xtac;;
+  tactical_wrap0 (x,[]) xttcl xtac;;
 
 let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic =
-  tactical_wrap0 (Some x, []) (xttcl xtac1) xtac2;;
+  tactical_wrap0 (x,[]) (xttcl xtac1) xtac2;;
 
 let int_tactical_wrap x (xttcl:int->'a->xtactic) (n:int) (xtac:'a) : xtactic =
-  tactical_wrap0 (Some x, [Fint n]) (xttcl n) xtac;;
+  tactical_wrap0 (x, [Mlint n]) (xttcl n) xtac;;
 
 let list_tactical_wrap x (xttcl:('a->xtactic)->'a list->xtactic)
                          (xtac:'a->xtactic) (l:'a list) : xtactic =
-  tactical_wrap0 (Some x, []) (xttcl xtac) l;;
+  tactical_wrap0 (x,[]) (xttcl xtac) l;;
 
 
 (* HILABEL *)
@@ -319,11 +334,11 @@ let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (xg:xgoal) : xgoalstate =
 
   let (asl,_) = g in
   let g2 = (asl,tm) in
-  let finfo = (Some "SUBGOAL_THEN",
-               [Fterm tm; (finfo_as_meta_arg o gtree_tactic) gtr0]) in
+  let obj = ("SUBGOAL_THEN",
+               [Mlterm tm; (mldata_as_meta_arg o gtree_tactic) gtr0]) in
 
   let (gs0,ids0) = unzip (map dest_xgoal xgs0) in
-  let xgs = extend_gtree id (Gbox (Tactical finfo, gtr0, true)) (g2::gs0) in
+  let xgs = extend_gtree id (Gbox (Tactical obj, gtr0, true)) (g2::gs0) in
   let ids1 = map xgoal_id (tl xgs) in
   let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in
   (do_list externalise_gtree (zip ids0 ids1);
diff --git a/hol-light/TacticRecording/xtactics.ml b/hol-light/TacticRecording/xtactics.ml
index 79b81648..fb7028c7 100644
--- a/hol-light/TacticRecording/xtactics.ml
+++ b/hol-light/TacticRecording/xtactics.ml
@@ -381,9 +381,11 @@ let (xTAC_PROOF : goal * xtactic -> thm) =
 let xprove(t,tac) =
   let th = xTAC_PROOF(([],t),tac) in
   let t' = concl th in
-  if t' = t then th else
-  try EQ_MP (ALPHA t' t) th
-  with Failure _ -> failwith "prove: justification generated wrong theorem";;
+  let th' =
+    if t' = t then th else
+    try EQ_MP (ALPHA t' t) th
+    with Failure _ -> failwith "prove: justification generated wrong theorem" in
+  mk_xthm (th', ("<tactic-proof>",[]))
 
 (* ------------------------------------------------------------------------- *)
 (* Subgoal package for xgoals.                                               *)
@@ -439,7 +441,7 @@ let xtop_goal() =
 
 let xtop_thm() =
   let (_,[],f)::_ = !current_xgoalstack in
-  f null_inst [];;
+  mk_xthm (f null_inst [], ("<tactic-proof>",[]));;
 
 (* ------------------------------------------------------------------------- *)
 (* Install the goal-related printers.                                        *)
diff --git a/hol-light/TacticRecording/xthm.ml b/hol-light/TacticRecording/xthm.ml
index 2619e03f..97fcec57 100644
--- a/hol-light/TacticRecording/xthm.ml
+++ b/hol-light/TacticRecording/xthm.ml
@@ -1,73 +1,40 @@
 
 
 
-(* ** DATATYPES ** *)
-
-
-type farg =
-   Fint of int
- | Fstring of string
- | Fterm of term
- | Ftype of hol_type
- | Fthm of finfo
- | Fpair of farg * farg
- | Flist of farg list
- | Ffn of finfo
-
-and finfo =
-   string option                     (* Function's name *)
- * farg list;;                       (* Function's args *)
-
-
-type label =
-   Tactical of finfo
- | Label of string;;
-
-
-(* Atomic tests *)
-
-let is_atomic_farg arg =
-  match arg with
-    Fthm (_,(_::_)) | Fpair _ -> false
-  | _ -> true;;
-
-let is_atomic_finfo ((x_,args):finfo) = (is_empty args);;
-
-
-(* active_info *)
-
-let active_info = (Some "...", []);;
+(* ** DATATYPE ** *)
 
 
 (* The 'xthm' datatype *)
 
-(* This couples a theorem with an 'finfo' representation of its proof.  For   *)
-(* named ML objects, this 'finfo' will simply be the ML name of the theorem.  *)
+(* This couples a theorem with an 'mldata' representation of its proof.  For  *)
+(* named ML objects, this 'mldata' will simply be the ML name of the theorem. *)
 (* For rule applications, it will capture the rule and its arguments.         *)
 
-type xthm = thm * finfo;;
+type xthm = thm * mldata;;
 
 type xconv = term -> xthm;;
 
 
 (* Constructors and destructors *)
 
-let mk_xthm (xth:thm*finfo) : xthm = xth;;
+let mk_xthm (xth:thm*mldata) : xthm = xth;;
 
-let mk_xthm0 x th = mk_xthm (th, (Some x, []));;
+let mk_xthm0 x th = mk_xthm (th, (x,[]));;
 
-let dest_xthm ((th,info):xthm) : thm * finfo = (th,info);;
+let dest_xthm ((th,prf):xthm) : thm * mldata = (th,prf);;
 
 let xthm_thm ((th,_):xthm) = th;;
 
-let xthm_proof ((_,info):xthm) = info;;
+let xthm_proof ((_,prf):xthm) = prf;;
+
+let name_xthm x ((th,_):xthm) : xthm = (th, (x,[]));;
 
 
 
 (* ** INSTALL PRINTERS ** *)
 
 
-let print_xthm ((th,info):xthm) = print_thm th;;
+let print_xthm ((th,_):xthm) = print_thm th;;
 
 #install_printer print_xthm;;