Various small improvements to capability

Whole of examples3 now processes
Facility for adding manual labels to atomic/composite tactics

9 files changed, 557 insertions, 302 deletions

diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml
index a8fcdb16..d0e181e2 100644
--- a/hol-light/TacticRecording/examples3.ml
+++ b/hol-light/TacticRecording/examples3.ml
@@ -5,6 +5,9 @@ needs "Library/products.ml";;
 
 prioritize_real();;
 
+AIM: CONT_COMPOSE (Library/analysis.ml)
+- used by John in his Proof Style paper
+
 
 (* ** LEMMA1 from HOL Light's 100/arithmetic_geometric_mean.ml ** *)
 
@@ -20,17 +23,50 @@ let LEMMA_1 = prove
   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);;
 
+let LEMMA_1 = prove
+ (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
+         (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
+  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
+   [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));;
+
 let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;;
 
 top_thm ();;
 print_executed_proof true;;
-print_flat_proof true;;
+print_flat_proof false;;
 print_packaged_proof ();;
+print_thenl_proof ();;
 
 g `!x n. x pow (n + 1) - (&n + &1) * x + &n =
          (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`;;
+e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
+e (GEN_TAC);;
+e (INDUCT_TAC);;
+(* *** Subgoal 1 *** *)
+e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
+e (REAL_ARITH_TAC);;
+(* *** Subgoal 2 *** *)
+e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
+e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
+e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
+e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
+e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
+e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
+e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
+e (REAL_ARITH_TAC);;
 
-print_executed_proof ();;
+print_executed_proof true;;
+print_packaged_proof ();;
+print_thenl_proof ();;
 
 (* LEMMA 2 *)
 
@@ -108,3 +144,30 @@ let AGM = prove
                  ARITH_RULE `i <= n ==> i <= n + 1`] THEN
     GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
     ASM_SIMP_TAC[LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]]);;
+
+g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
+         ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;;
+e (INDUCT_TAC);;
+(* *** Subgoal 1 *** *)
+e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);;
+(* *** Subgoal 2 *** *)
+e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);;
+e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
+e (X_GEN_TAC `x:num->real`);;
+e (ASM_CASES_TAC `n = 0`);;
+(* *** Subgoal 2.1 *** *)
+e (ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG]);;
+e (REAL_ARITH_TAC);;
+(* *** Subgoal 2.2 *** *)
+e (REWRITE_TAC [ADD1]);;
+e (STRIP_TAC);;
+e (MATCH_MP_TAC REAL_LE_TRANS);;
+e (EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n`);;
+e (ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]);;
+e (GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM]);;
+e (MATCH_MP_TAC REAL_LE_RMUL);;
+e (ASM_SIMP_TAC [LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]);;
+
+g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
+         ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;;
+e (INDUCT_TAC THEN REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG] THEN REWRITE_TAC [ARITH_RULE `1 <= SUC n`] THEN X_GEN_TAC `x:num->real` THEN ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG] THEN REAL_ARITH_TAC; REWRITE_TAC [ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n` THEN ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_RMUL THEN ASM_SIMP_TAC [LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]]);;
diff --git a/hol-light/TacticRecording/examples5.ml b/hol-light/TacticRecording/examples5.ml
new file mode 100644
index 00000000..6e34aaee
--- /dev/null
+++ b/hol-light/TacticRecording/examples5.ml
@@ -0,0 +1,79 @@
+from Library/binomial.ml
+
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* Binomial coefficients.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+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;;
+
+(* ------------------------------------------------------------------------- *)
+(* More potentially useful lemmas.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+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;;
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml
index b48dd2da..41941cde 100644
--- a/hol-light/TacticRecording/hiproofs.ml
+++ b/hol-light/TacticRecording/hiproofs.ml
@@ -30,7 +30,7 @@ type hiproof =
     Hactive                             (* Active subgoal *)
   | Hatomic of (finfo * int)            (* Atomic tactic + arity *)
   | Hidentity                           (* Null, for wiring *)
-  | Hlabelled of (finfo * hiproof)      (* Box *)
+  | Hlabelled of (label * hiproof)      (* Box *)
   | Hsequence of (hiproof * hiproof)    (* Serial application *)
   | Htensor of hiproof list             (* Parallel application *)
   | Hempty;;                            (* Completed goal *)
@@ -87,9 +87,9 @@ type hitrace =
 let rec refactor_hiproof r foo h =
   let h' =
      match h with
-       Hlabelled (info,h0)
+       Hlabelled (l,h0)
           -> let h0' = refactor_hiproof r foo h0 in
-             Hlabelled (info,h0')
+             Hlabelled (l,h0')
      | Hsequence (h1,h2)
           -> let h1' = refactor_hiproof r foo h1 in
              let h2' = refactor_hiproof r foo h2 in
@@ -169,7 +169,7 @@ let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
 let delabel_hiproof h =
   let delabel h =
      match h with
-       Hlabelled ((Some "SUBGOAL_THEN",_),h0)
+       Hlabelled (Tactical (Some "SUBGOAL_THEN",_), h0)
           -> h
      | Hlabelled (_,h0)
           -> h0
@@ -221,12 +221,12 @@ let thenise_hiproof h =
      match h with
        Hsequence (h1, Htensor (h2::h2s))
           -> if (forall (fun h0 -> h0 = h2) h2s)
-               then Hlabelled ((Some "THEN", []), h)
+               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 ((Some "THEN", []),
+                     (Hlabelled (Tactical (Some "THEN", []),
                                  Hsequence (h1, Htensor (h2::h2s))), h3)
                else h
      | _  -> h in
@@ -250,7 +250,7 @@ let rec hiproof_tactic_trace0 h =
        -> [info]
   | Hidentity
        -> []
-  | Hlabelled (info,h0)
+  | Hlabelled (_,h0)
        -> hiproof_tactic_trace0 h0
   | Hsequence (h1,h2)
        -> (hiproof_tactic_trace0 h1) @ (hiproof_tactic_trace0 h2)
diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml
index 2dd6e6ef..44c01951 100644
--- a/hol-light/TacticRecording/main.ml
+++ b/hol-light/TacticRecording/main.ml
@@ -1,14 +1,25 @@
+(* Library stuff *)
 
 #use "TacticRecording/lib.ml";;
 #use "TacticRecording/dltree.mli";;
 #use "TacticRecording/dltree.ml";;
 
+(* Datatypes and recording mechanism *)
+
 #use "TacticRecording/xthm.ml";;
 #use "TacticRecording/xtactics.ml";;
 #use "TacticRecording/tacticrec.ml";;
+#use "TacticRecording/wrappers.ml";;
+
+(* Prooftree support *)
+
 #use "TacticRecording/prooftree.ml";;
 
+(* Hiproofs, refactoring and export *)
+
 #use "TacticRecording/hiproofs.ml";;
 #use "TacticRecording/mlexport.ml";;
 
+(* Overwriting the existing HOL Light objects *)
+
 #use "TacticRecording/promote.ml";;
diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml
index ba26034a..d790deee 100644
--- a/hol-light/TacticRecording/mlexport.ml
+++ b/hol-light/TacticRecording/mlexport.ml
@@ -24,10 +24,10 @@ let rec gtree_to_hiproof gtr =
   | Gexecuted (gstp,gtrs)
        -> let h1 =
              match gstp with
-               Gatom info | Gbox (info,_,true)
+               Gatom info | Gbox (Tactical info, _, true)
                   -> Hatomic (info, length gtrs)
-             | Gbox (info,gtr,false)
-                  -> Hlabelled (info, gtree_to_hiproof gtr) in
+             | Gbox (l,gtr,false)
+                  -> Hlabelled (l, gtree_to_hiproof gtr) in
           let h2 = Htensor (map gtree_to_hiproof gtrs) in
           Hsequence (h1,h2);;
 
@@ -122,7 +122,7 @@ let print_hiproof0 pr br h =
        -> print_tactic br info
   | Hidentity
        -> print_string "ALL_TAC"
-  | Hlabelled (info,h0)
+  | Hlabelled (_,h0)
        -> pr br h0
   | Hsequence (h1, Htensor h2s)
        -> (print_string_if br "(";
@@ -154,20 +154,28 @@ let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;;
 
 let rec print_hiproof2 br h =
   match h with
-    Hlabelled ((Some "REPEAT", _), Hsequence (h1,h2))  (* only if repeats *)
+    Hlabelled (Tactical (Some "REPEAT", _), Hsequence (h1,h2)) (* if repeated *)
        -> (print_string_if br "(";
            print_string "REPEAT ";
            print_hiproof2 true h1;
            print_string_if br ")")
-  | Hlabelled ((Some "THEN", _),
-               Hsequence (h1, Htensor (h2::h2s)))      (* only if tac2 used *)
+  | Hlabelled (Tactical (Some "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 (((Some "SUBGOAL_THEN", (Fterm tm)::[farg]) as info), _)
+  | Hlabelled (Tactical ((Some "SUBGOAL_THEN",                (* special case *)
+                         (Fterm tm)::[farg]) as info),
+               _)
        -> (print_tactic br info)
+  | Hlabelled (Label x, h)
+       -> (print_string_if br "(";
+           print_string "HILABEL ";
+           print_fstring x; print_string " ";
+           print_hiproof2 true h;
+           print_string_if br ")")
   | _  -> (print_hiproof0 print_hiproof2 br h);;
 
 
diff --git a/hol-light/TacticRecording/promote.ml b/hol-light/TacticRecording/promote.ml
index 0b40b5f9..cd711707 100644
--- a/hol-light/TacticRecording/promote.ml
+++ b/hol-light/TacticRecording/promote.ml
@@ -24,6 +24,8 @@ let ASSUME_TAC = thm_tactic_wrap "ASSUME_TAC" ASSUME_TAC;;
 
 let ACCEPT_TAC = thm_tactic_wrap "ACCEPT_TAC" ACCEPT_TAC;;
 
+let CONV_TAC = conv_tactic_wrap "CONV_TAC" CONV_TAC;;
+
 let REFL_TAC = tactic_wrap "REFL_TAC" REFL_TAC;;
 let ABS_TAC = tactic_wrap "ABS_TAC" ABS_TAC;;
 let MK_COMB_TAC = tactic_wrap "MK_COMB_TAC" MK_COMB_TAC;;
@@ -65,7 +67,6 @@ let ANTS_TAC = tactic_wrap "ANTS_TAC" ANTS_TAC;;
 
 (* Special cases, already fully hand-promoted *)
 
-let CONV_TAC = xCONV_TAC;;
 let SUBGOAL_THEN = xSUBGOAL_THEN;;
 
 
@@ -218,6 +219,8 @@ let PURE_ASM_REWRITE_TAC =
         thmlist_tactic_wrap "PURE_ASM_REWRITE_TAC" PURE_ASM_REWRITE_TAC;;
 let ONCE_ASM_REWRITE_TAC =
         thmlist_tactic_wrap "ONCE_ASM_REWRITE_TAC" ONCE_ASM_REWRITE_TAC;;
+let GEN_REWRITE_TAC =
+        convconvthmlist_tactic_wrap "GEN_REWRITE_TAC" GEN_REWRITE_TAC;;
 let SIMP_TAC = thmlist_tactic_wrap "SIMP_TAC" SIMP_TAC;;
 let PURE_SIMP_TAC = thmlist_tactic_wrap "PURE_SIMP_TAC" PURE_SIMP_TAC;;
 let ONCE_SIMP_TAC = thmlist_tactic_wrap "ONCE_SIMP_TAC" ONCE_SIMP_TAC;;
@@ -241,12 +244,20 @@ let ASM_REAL_ARITH_TAC = tactic_wrap "ASM_REAL_ARITH_TAC" ASM_REAL_ARITH_TAC;;
 
 (* More rules *)
 
+let RATOR_CONV = conv_conv_wrap "RATOR_CONV" RATOR_CONV;;
+let RAND_CONV = conv_conv_wrap "RAND_CONV" RAND_CONV;;
+let LAND_CONV = conv_conv_wrap "LAND_CONV" LAND_CONV;;
+let ABS_CONV = conv_conv_wrap "ABS_CONV" ABS_CONV;;
+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 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 num_CONV = conv_wrap "num_CONV" num_CONV;;
 let ARITH_RULE = conv_wrap "ARITH_RULE" ARITH_RULE;;
 
 let REAL_ARITH = conv_wrap "REAL_ARITH" REAL_ARITH;;
@@ -262,9 +273,13 @@ 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_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;;
+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 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 FACT = theorem_wrap "FACT" FACT;;
 
 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;;
@@ -294,4 +309,5 @@ let SUM_ADD_SPLIT = theorem_wrap "SUM_ADD_SPLIT" SUM_ADD_SPLIT;;
 let SUM_POS_LE_NUMSEG = theorem_wrap "SUM_POS_LE_NUMSEG" SUM_POS_LE_NUMSEG;;
 let SUM_CLAUSES_NUMSEG = theorem_wrap "SUM_CLAUSES_NUMSEG" SUM_CLAUSES_NUMSEG;;
 let SUM_SING_NUMSEG = theorem_wrap "SUM_SING_NUMSEG" SUM_SING_NUMSEG;;
-let PRODUCT_CLAUSES_NUMSEG = theorem_wrap "PRODUCT_CLAUSES_NUMSEG" PRODUCT_CLAUSES_NUMSEG;;
\ No newline at end of file
+let PRODUCT_CLAUSES_NUMSEG =
+   theorem_wrap "PRODUCT_CLAUSES_NUMSEG" PRODUCT_CLAUSES_NUMSEG;;
\ No newline at end of file
diff --git a/hol-light/TacticRecording/tacticrec.ml b/hol-light/TacticRecording/tacticrec.ml
index 0836f87c..7df77fad 100644
--- a/hol-light/TacticRecording/tacticrec.ml
+++ b/hol-light/TacticRecording/tacticrec.ml
@@ -61,7 +61,7 @@ type ginfo =
 
 type gstep =
    Gatom of finfo                    (* Atomic tactic *)
- | Gbox of (finfo * gtree * bool)    (* Box for a tactical; flag for special *)
+ | Gbox of (label * gtree * bool)    (* Box for a tactical; flag for special *)
 
 and gtree0 =
    Gactive                                                (* Active goal *)
@@ -80,7 +80,7 @@ and gtree =
 (*                                                                            *)
 (*  (_, ref                                                                   *)
 (*   Gexecuted                                                                *)
-(*     (Gbox (Some "T1")                                                      *)
+(*     (Gbox (Tactical (Some "T1"))                                           *)
 (*        (_, ref                                                             *)
 (*         Gexecuted                                                          *)
 (*           (Gatom (Some "T2"),                                              *)
@@ -88,7 +88,7 @@ and gtree =
 (*              (_, ref Gexit _) ])),                                         *)
 (*      [ (_, ref                                                             *)
 (*         Gexecuted                                                          *)
-(*           (Gbox (Some "DP")                                                *)
+(*           (Gbox (Tactical (Some "DP"))                                     *)
 (*              (_, ref                                                       *)
 (*               Gexecuted                                                    *)
 (*                 (Gatom (Some "Normalise"),                                 *)
@@ -125,7 +125,8 @@ let gtree_fproof ((info,_):gtree) = ginfo_fproof info;;
 
 let gstep_tactic (gstp:gstep) =
   match gstp with
-    Gatom info | Gbox (info,_,_) -> info;;
+    Gatom info | Gbox (Tactical info, _, true) -> info
+  | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";;
 
 let gtree_proof ((_,gtrm):gtree) =
   match (!gtrm) with
@@ -206,8 +207,8 @@ let rec gtree_all_children gtr =
 
 and gstep_all_children gstp =
   match gstp with
-    Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr)
-  | Gatom _ | Gbox _   -> [];;
+    Gatom _ | Gbox (_,_,true) -> []
+  | Gbox (_,gtr,false)        -> gtr::(gtree_all_children gtr);;
 
 
 
@@ -243,9 +244,9 @@ let extend_gtree (pid:goalid) (gstp:gstep) (gs':goal list) : xgoal list =
            with Assert_failure _ ->
                    failwith "extend_gtree: Internal error - Not active" in
   let (ids',gtrs) = unzip (map (new_active_subgtree pid) gs') in
-  let gxs' = zip gs' ids' in
+  let xgs' = zip gs' ids' in
   (gtrm := Gexecuted (gstp,gtrs);
-   gxs');;
+   xgs');;
 
 
 (* Deletion *)
@@ -276,153 +277,6 @@ let externalise_gtree ((id0,id):goalid*goalid) : unit =
 
 
 
-(* ** WRAPPER FUNCTIONS ** *)
-
-(* These functions are for promoting existing tactics and tacticals.          *)
-
-
-(* Tactic wrapper *)
-
-(* 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 finfo (tac:tactic) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let (meta,gs',just) = tac g in
-  let gxs' = extend_gtree id (Gatom finfo) gs' in
-  (meta,gxs',just);;
-
-let tactic_wrap x tac =
-  tactic_wrap0 (Some x, []) tac;;
-
-let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic =
-  tactic_wrap0 (Some x, [Fstring s]) (tac s);;
-
-let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic =
-  tactic_wrap0 (Some x, [Fterm 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));;
-
-let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic =
-  tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm 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);;
-
-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);;
-
-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);;
-
-
-(* xCONV_TAC - a special case I think; not a tactical *)
-
-let t_tm = `T`;;
-
-let xCONV_TAC (cx:xconv) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-
-  let (asl,w) = g in
-  let thx = cx w in
-  let (th,proof) = dest_xthm thx in
-  let tm = concl th in
-  let finfo = (Some "CONV_TAC", [finfo_as_meta_arg proof]) in
-
-  let tac g =
-     if (aconv tm w)
-       then (null_meta, [], fun i [] -> INSTANTIATE_ALL i th)
-     else let l,r = dest_eq tm in
-       if not (aconv l w)
-       then failwith "CONV_TAC: bad equation"
-     else if (r = t_tm)
-       then (null_meta, [], fun i [] -> INSTANTIATE_ALL i (EQT_ELIM th))
-       else (null_meta, [(asl,r)],
-             fun i [th0] -> EQ_MP (INSTANTIATE_ALL i (SYM th)) th0) in
-
-  let (meta,gs,just) = tac g in
-  let gxs = extend_gtree id (Gatom finfo) gs in
-  (meta,gxs,just);;
-
-
-(* Tactical wrapper *)
-
-(* This is for wrapping around a tactical, to incorporate the results into a  *)
-(* box in an existing gtree, where the execution of the tactical's tactics is *)
-(* captured inside the box, so that they can be stepped through and/or        *)
-(* refactored.  Thus we cannot take the tactical as a black box; it must      *)
-(* 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 finfo (xttcl:'a->xtactic) (arg:'a) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let (id0,gtr0) = new_active_subgtree id g in
-  let gx0 = mk_xgoal (g,id0) in
-  let (meta,gxs0,just) = xttcl arg gx0 in
-  let (gs0,ids0) = unzip (map dest_xgoal gxs0) in
-  let gxs = extend_gtree id (Gbox (finfo,gtr0,false)) gs0 in
-  let ids = map xgoal_id gxs in
-  (do_list externalise_gtree (zip ids0 ids);
-   (meta,gxs,just));;
-
-let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic =
-  tactical_wrap0 (Some x, []) xttcl xtac;;
-
-let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic =
-  tactical_wrap0 (Some 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;;
-
-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;;
-
-
-(* xSUBGOAL_THEN - seems to be another special case *)
-
-let xASSUME = conv_wrap "ASSUME" ASSUME;;
-
-let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (gx:xgoal) : xgoalstate =
-  let arg = xASSUME tm in
-
-  let (g,id) = dest_xgoal gx in
-  let (id0,gtr0) = new_active_subgtree id g in
-  let gx0 = mk_xgoal (g,id0) in
-  let (meta,gxs0,just) = ttac arg gx0 in
-  let (gs0,ids0) = unzip (map dest_xgoal gxs0) in
-
-  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 gxs = extend_gtree id (Gbox (finfo,gtr0,true)) (g2::gs0) in
-  let ids1 = map xgoal_id (tl gxs) in
-  let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in
-  (do_list externalise_gtree (zip ids0 ids1);
-   (meta,gxs,just'));;
-
-
-(*
-let SUBGOAL_TAC s tm prfs =
-  match prfs with
-   p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored";
-             SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC])
-  | [] -> failwith "SUBGOAL_TAC: no subproof given";;
-
-let (FREEZE_THEN :thm_tactical) =
-  fun ttac th (asl,w) ->
-    let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in
-    meta,gl,fun i l -> PROVE_HYP th (just i l);;
-*)
-
-
-
 (* ** SUBGOAL PACKAGE OPERATIONS FOR XGOALS ** *)
 
 (* A few of the xtactic subgoal package commands are adjusted here.           *)
@@ -470,12 +324,12 @@ let xg t =
 
 (* Undoing a tactic proof step *)
 
-(* 'xb' needs to be adjusted to deleted the undone step in the goal tree.     *)
+(* 'xb' needs to be adjusted to delete the undone step in the goal tree.      *)
 
 let xb () =
   let result = xb () in
-  let (_,gxs,_) = hd result in
-  let (_,id) = hd gxs in
+  let (_,xgs,_) = hd result in
+  let (_,id) = hd xgs in
   (delete_step id;
    result);;
 
diff --git a/hol-light/TacticRecording/wrappers.ml b/hol-light/TacticRecording/wrappers.ml
new file mode 100644
index 00000000..1244c89f
--- /dev/null
+++ b/hol-light/TacticRecording/wrappers.ml
@@ -0,0 +1,344 @@
+(* ========================================================================== *)
+(* WRAPPER FUNCTIONS (HOL LIGHT)                                              *)
+(* - Functions for promoting thm/goal-related ML objects for xthm/xgoal       *)
+(*                                                                            *)
+(* By Mark Adams                                                              *)
+(* Copyright (c) Univeristy of Edinburgh, 2011-2012                           *)
+(* ========================================================================== *)
+
+
+
+(* ** THEOREM-RELATED WRAPPER FUNCTIONS ** *)
+
+
+(* finfo_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 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";;
+
+
+(* detect_rule_app *)
+
+(* Based on the assumption that the given meta function actually executes its *)
+(* rule argument at some point, this utility detects such an execution during *)
+(* the demotion of a given xrule argument to a rule.  The meta function's     *)
+(* 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 r arg = let xth = xr arg in
+              let (th,info) = dest_xthm xth in
+              (temp := finfo_as_meta_arg info;
+               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 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 xth = xmr xmarg arg in
+                    let (th,info) = dest_xthm xth in
+                    (temp := finfo_as_meta2_arg info;
+                     th) in
+  let th = mfunc mr in
+  (th,!temp);;
+
+
+(* Theorem wrapper *)
+
+let theorem_wrap (x:string) (th:thm) : xthm =
+  (th, (Some x, []));;
+
+
+(* Rule wrappers *)
+
+(* 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 th' = r arg in
+  mk_xthm (th',finfo);;
+
+let conv_wrap x (r:term->thm) (tm:term) : xthm =
+  rule_wrap0 (Some x, [Fterm 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;;
+
+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])
+             (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;;
+
+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;;
+
+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);;
+
+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;;
+
+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;;
+
+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;;
+
+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;;
+
+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])
+             (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])
+             (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])
+             (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])
+             (r ths) 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 conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm =
+  meta_rule_wrap0 (Some x, [Fterm tm]) mc xc tm;;
+
+
+
+(* ** TACTIC-RELATED WRAPPER FUNCTIONS ** *)
+
+(* These functions are for promoting existing tactics and tacticals.          *)
+
+
+(* Generic basic wrapper util *)
+
+(* Applies a tactic and incorproates the results into the goal tree.  Takes   *)
+(* an "infotactic", i.e. like a normal tactic that works on 'goal' and        *)
+(* 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 (g,id) = dest_xgoal xg in
+  let ((meta,gs,just),info) = infotac g in
+  let xgs = extend_gtree id (Gatom info) gs in
+  (meta,xgs,just);;
+
+
+(* Generic box wrapper util *)
+
+(* Sets up a box to apply an xtactic within, applies the xtactic (which       *)
+(* incorporates itself into the goal tree) and wires up the resulting         *)
+(* subgoals to external subgoals of the box.  Note that this is not quite     *)
+(* generic enough for 'SUBGOAL_THEN' (because there is not a total surjection *)
+(* between internal and external goals).                                      *)
+
+let infobox_wrap (xinfotac:xgoal->xgoalstate*label) (xg:xgoal) : xgoalstate =
+  let (g,id) = dest_xgoal xg in
+  let (id0,gtr0) = new_active_subgtree id g in
+  let xg0 = mk_xgoal (g,id0) in
+  let ((meta,xgs0,just),l) = xinfotac xg0 in
+  let (gs0,ids0) = unzip (map dest_xgoal xgs0) in
+  let xgs = extend_gtree id (Gbox (l,gtr0,false)) gs0 in
+  let ids = map xgoal_id xgs in
+  (do_list externalise_gtree (zip ids0 ids);
+   (meta,xgs,just));;
+
+
+(* Tactic wrapper *)
+
+(* 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
+  infotactic_wrap infotac;;
+
+let tactic_wrap x tac =
+  tactic_wrap0 (Some x, []) tac;;
+
+let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic =
+  tactic_wrap0 (Some x, [Fstring s]) (tac s);;
+
+let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic =
+  tactic_wrap0 (Some x, [Fterm 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));;
+
+let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic =
+  tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm 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);;
+
+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);;
+
+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);;
+
+
+(* Meta-tactic wrapper *)
+
+(* For tactics that take rule arguments.                                      *)
+
+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
+  infotactic_wrap infotac;;
+
+let conv_tactic_wrap x (mtac:conv->tactic) (xc:xconv) : xtactic =
+  meta_tactic_wrap0 (Some 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
+  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)])
+                       (fun mc -> mmtac mc ths)
+                       xmc;;
+
+
+(* Tactical wrapper *)
+
+(* This is for wrapping around a tactical, to incorporate the results into a  *)
+(* box in an existing gtree, where the execution of the tactical's tactics is *)
+(* captured inside the box, so that they can be stepped through and/or        *)
+(* refactored.  Thus we cannot take the tactical as a black box; it must      *)
+(* 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
+  infobox_wrap xinfotac;;
+
+let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic =
+  tactical_wrap0 (Some x, []) xttcl xtac;;
+
+let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic =
+  tactical_wrap0 (Some 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;;
+
+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;;
+
+
+(* HILABEL *)
+
+(* Command for putting the result of a tactic into a box and giving the box a *)
+(* label (distinct from a tactical label).                                    *)
+
+let HILABEL x (xtac:xtactic) : xtactic =
+  let xinfotac xg = (xtac xg, Label x) in
+  infobox_wrap xinfotac;;
+
+
+(* xSUBGOAL_THEN - seems to be a special case *)
+
+let xASSUME = conv_wrap "ASSUME" ASSUME;;
+
+let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (xg:xgoal) : xgoalstate =
+  let arg = xASSUME tm in
+
+  let (g,id) = dest_xgoal xg in
+  let (id0,gtr0) = new_active_subgtree id g in
+  let xg0 = mk_xgoal (g,id0) in
+  let (meta,xgs0,just) = ttac arg xg0 in
+
+  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 (gs0,ids0) = unzip (map dest_xgoal xgs0) in
+  let xgs = extend_gtree id (Gbox (Tactical finfo, 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);
+   (meta,xgs,just'));;
+
+
+(*
+let SUBGOAL_TAC s tm prfs =
+  match prfs with
+   p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored";
+             SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC])
+  | [] -> failwith "SUBGOAL_TAC: no subproof given";;
+
+let (FREEZE_THEN :thm_tactical) =
+  fun ttac th (asl,w) ->
+    let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in
+    meta,gl,fun i l -> PROVE_HYP th (just i l);;
+*)
diff --git a/hol-light/TacticRecording/xthm.ml b/hol-light/TacticRecording/xthm.ml
index 210530fa..2619e03f 100644
--- a/hol-light/TacticRecording/xthm.ml
+++ b/hol-light/TacticRecording/xthm.ml
@@ -19,13 +19,9 @@ and finfo =
  * farg list;;                       (* Function's args *)
 
 
-(* finfo_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";;
+type label =
+   Tactical of finfo
+ | Label of string;;
 
 
 (* Atomic tests *)
@@ -60,127 +56,11 @@ let mk_xthm (xth:thm*finfo) : xthm = xth;;
 
 let mk_xthm0 x th = mk_xthm (th, (Some x, []));;
 
-let dest_xthm ((th,x):xthm) : thm * finfo = (th,x);;
+let dest_xthm ((th,info):xthm) : thm * finfo = (th,info);;
 
 let xthm_thm ((th,_):xthm) = th;;
 
-let xthm_proof ((_,prf):xthm) = prf;;
-
-
-
-(* ** WRAPPER FUNCTIONS ** *)
-
-
-(* Theorem wrapper *)
-
-let theorem_wrap (x:string) (th:thm) : xthm =
-  (th, (Some x, []));;
-
-
-(* Rule wrappers *)
-
-(* 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 th' = r arg in
-  mk_xthm (th',finfo);;
-
-let conv_wrap x (r:term->thm) (tm:term) : xthm =
-  rule_wrap0 (Some x, [Fterm tm]) r tm;;
-
-let thm_conv_wrap x (r:thm->term->thm) (thx:xthm) tm : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;;
-
-let thmlist_conv_wrap x (r:thm list->term->thm) thxs (tm:term) : xthm =
-  let (ths,prfs) = unzip (map dest_xthm thxs) in
-  rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm])
-             (r ths) tm;;
-
-let rule_wrap x (r:thm->thm) (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Fthm prf]) r th;;
-
-let drule_wrap x (r:thm->thm->thm) (thx1:xthm) (thx2:xthm) : xthm =
-  let (th1,prf1) = dest_xthm thx1 in
-  let (th2,prf2) = dest_xthm thx2 in
-  rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;;
-
-let prule_wrap x (r:thm*thm->thm) ((thx1:xthm),(thx2:xthm)) : xthm =
-  let (th1,prf1) = dest_xthm thx1 in
-  let (th2,prf2) = dest_xthm thx2 in
-  rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);;
-
-let trule_wrap x (r:thm->thm->thm->thm)
-                 (thx1:xthm) (thx2:xthm) (thx3:xthm) : xthm =
-  let (th1,prf1) = dest_xthm thx1 in
-  let (th2,prf2) = dest_xthm thx2 in
-  let (th3,prf3) = dest_xthm thx3 in
-  rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;;
-
-let term_rule_wrap x (r:term->thm->thm) tm (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;;
-
-let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;;
-
-let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,thx0) (thx:xthm) : xthm =
-  let (th0,prf0) = dest_xthm thx0 in
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;;
-
-let termlist_rule_wrap x (r:term list->thm->thm) tms (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf])
-             (r tms) th;;
-
-let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x,
-              [Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta);
-               Fthm prf])
-             (r theta) th;;
-
-let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm)
-                         theta (thx:xthm) : xthm =
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x,
-              [Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta);
-               Fthm prf])
-             (r theta) th;;
-
-let thmlist_rule_wrap x (r:thm list->thm->thm) thxs (thx:xthm) : xthm =
-  let (ths,prfs) = unzip (map dest_xthm thxs) in
-  let (th,prf) = dest_xthm thx in
-  rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf])
-             (r ths) th;;
-
-
-(* Meta rule wrappers *)
-
-(* This works by ... *)
-(* Fails to give a meta argument if it never gets executed.                   *)
-
-let meta_rule_wrap0 finfo0 (mr:('a->thm)->'b->thm)
-                           (xr:'a->xthm) (arg:'b) : xthm =
-  let temp = ref ((Some "???", []) : finfo) in
-  let r arg0 = let thx = xr arg0 in
-               let (th,finfo) = dest_xthm thx in
-               ((match finfo with
-                   (x_, (_::_ as args))
-                      -> (temp := (x_, front args))
-                 | _  -> ());
-                th) in
-  let th' = mr r arg in
-  let (x_,args0) = finfo0 in
-  let finfo' = (x_, (Ffn !temp)::args0) in
-  (th',finfo');;
-
-let conv_conv_wrap x (mc:conv->conv) (c:term->xthm) (tm:term) : xthm =
-  meta_rule_wrap0 (Some x, [Fterm tm]) mc c tm;;
+let xthm_proof ((_,info):xthm) = info;;