diff --git a/examples/probability/Holmakefile b/examples/probability/Holmakefile
index 58822d8acc..0b1641862e 100644
--- a/examples/probability/Holmakefile
+++ b/examples/probability/Holmakefile
@@ -1,5 +1,7 @@
 INCLUDES = $(HOLDIR)/src/probability $(HOLDIR)/src/n-bit $(HOLDIR)/src/real \
-	   $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/analysis
+	   $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/analysis legacy
+
+CLINE_OPTIONS = -r
 
 EXTRA_CLEANS = heap \
 	$(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS)) \
@@ -17,7 +19,8 @@ FULL_OBJPATHS = $(patsubst %,$(HOLDIR)/src/%.uo,$(OBJS)) \
 all: $(HOLHEAP)
 
 $(HOLHEAP): $(FULL_OBJPATHS) $(HOLDIR)/bin/hol.state
-	$(protect $(HOLDIR)/bin/buildheap) -o $@ $(FULL_OBJPATHS)
+	$(protect $(HOLDIR)/bin/buildheap) $(DEBUG_FLAG) -o $@ \
+            -b $(protect $(HOLDIR)/src/real/analysis/realheap) $(FULL_OBJPATHS)
 endif
 
 all: $(DEFAULT_TARGETS)
diff --git a/examples/probability/legacy/Holmakefile b/examples/probability/legacy/Holmakefile
index 160cfb5e18..e95edce1d6 100644
--- a/examples/probability/legacy/Holmakefile
+++ b/examples/probability/legacy/Holmakefile
@@ -3,6 +3,8 @@ INCLUDES = $(HOLDIR)/src/real $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/anal
 
 EXTRA_CLEANS = $(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
 
+HOLHEAP = $(protect $(HOLDIR)/src/real/analysis/realheap)
+
 all: $(DEFAULT_TARGETS)
 
 .PHONY: all
diff --git a/src/probability/lebesgueScript.sml b/src/probability/lebesgueScript.sml
index 350c6a1e5e..e1c8514a4a 100644
--- a/src/probability/lebesgueScript.sml
+++ b/src/probability/lebesgueScript.sml
@@ -7343,7 +7343,7 @@ val suminf_measure = prove (
          (suminf (\i. measure M (A i)) = measure M (BIGUNION {A i | i IN UNIV}))``,
     RW_TAC std_ss [GSYM IMAGE_DEF]
  >> MATCH_MP_TAC (SIMP_RULE std_ss [o_DEF] MEASURE_COUNTABLY_ADDITIVE)
- >> FULL_SIMP_TAC std_ss [IN_FUNSET, disjoint_family_on, disjoint_family]
+ >> FULL_SIMP_TAC std_ss [IN_FUNSET, disjoint_family_on]
  >> ASM_SET_TAC []);
 
 (* removed ‘image_measure_space’, reduced ‘N’ (measure_space) to ‘B’ (sigma_algebra) *)
@@ -7366,7 +7366,7 @@ Proof
  >> `BIGUNION {PREIMAGE t (A i) INTER m_space M | i IN UNIV} IN measurable_sets M`
       by (FULL_SIMP_TAC std_ss [sigma_algebra_alt])
  >> `disjoint_family (\i. PREIMAGE t (A i) INTER m_space M)`
-      by (FULL_SIMP_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] \\
+      by (FULL_SIMP_TAC std_ss [disjoint_family_on, IN_UNIV] \\
           FULL_SIMP_TAC std_ss [PREIMAGE_def] THEN ASM_SET_TAC [])
  >> SIMP_TAC std_ss [PREIMAGE_BIGUNION, o_DEF]
  >> Know `IMAGE (PREIMAGE t) {A i | i IN univ(:num)} =
@@ -9478,7 +9478,7 @@ Proof
    suminf (\j. indicator_fn ((\i'. s INTER A i') j) x)` THENL
   [DISCH_TAC THEN ASM_SIMP_TAC std_ss [],
    GEN_TAC THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC indicator_fn_suminf THEN
-  FULL_SIMP_TAC std_ss [disjoint_family, disjoint_family_on, DISJOINT_DEF] THEN
+  FULL_SIMP_TAC std_ss [disjoint_family_on, DISJOINT_DEF] THEN
   ASM_SET_TAC []] THEN ONCE_REWRITE_TAC [METIS [ETA_AX]
    ``(\x'. indicator_fn (s INTER A x) x') = (\x. indicator_fn (s INTER A x)) x``] THEN
   ONCE_REWRITE_TAC [METIS [] ``suminf (\j. indicator_fn (s INTER A j) x) =
@@ -9844,7 +9844,7 @@ Proof
    SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE, subsets_def, GSPECIFICATION] THEN
    GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN METIS_TAC [], ALL_TAC] THEN
   CONJ_TAC THENL
-  [SIMP_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] THEN
+  [SIMP_TAC std_ss [disjoint_family_on, IN_UNIV] THEN
    REPEAT STRIP_TAC THEN Q.UNABBREV_TAC `QQ` THEN BETA_TAC THEN
    SIMP_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] THEN
    GEN_TAC THEN REPEAT COND_CASES_TAC THENL (* 4 subgoals *)
@@ -10155,7 +10155,7 @@ Proof
           suminf (\j. indicator_fn ((\i'. Q i INTER A i') j) x)` THENL
        [DISCH_TAC THEN ASM_SIMP_TAC std_ss [],
         GEN_TAC THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC indicator_fn_suminf THEN
-        FULL_SIMP_TAC std_ss [disjoint_family, disjoint_family_on, DISJOINT_DEF] THEN
+        FULL_SIMP_TAC std_ss [disjoint_family_on, DISJOINT_DEF] THEN
         ASM_SET_TAC []] THEN ONCE_REWRITE_TAC [METIS [ETA_AX]
           ``(\x'. indicator_fn (Q i INTER A x) x') = (\x. indicator_fn (Q i INTER A x)) x``] THEN
        ONCE_REWRITE_TAC [METIS [] ``suminf (\j. indicator_fn (Q i INTER A j) x) =
@@ -10190,7 +10190,7 @@ Proof
            suminf (\j. indicator_fn ((\i'. Q i INTER A i') j) x)` THENL
    [DISCH_TAC THEN ASM_SIMP_TAC std_ss [],
     GEN_TAC THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC indicator_fn_suminf THEN
-    FULL_SIMP_TAC std_ss [disjoint_family, disjoint_family_on, DISJOINT_DEF] THEN
+    FULL_SIMP_TAC std_ss [disjoint_family_on, DISJOINT_DEF] THEN
     ASM_SET_TAC []] THEN ONCE_REWRITE_TAC [METIS [ETA_AX]
      ``(\x'. indicator_fn (Q i INTER A x) x') = (\x. indicator_fn (Q i INTER A x)) x``] THEN
    ONCE_REWRITE_TAC [METIS [] ``suminf (\j. indicator_fn (Q i INTER A j) x) =
@@ -10521,7 +10521,7 @@ Proof
     METIS_TAC [ALGEBRA_INTER, subsets_def, measure_space_def, sigma_algebra_def],
     ALL_TAC] THEN
    CONJ_TAC THENL
-   [ASM_SET_TAC [DISJOINT_DEF, disjoint_family, disjoint_family_on], ALL_TAC] THEN
+   [ASM_SET_TAC [DISJOINT_DEF, disjoint_family_on], ALL_TAC] THEN
    ONCE_REWRITE_TAC [METIS [subsets_def] ``measurbale_sets M =
                        subsets (m_space M, measurbale_sets M)``] THEN
    MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION THEN
@@ -10600,10 +10600,10 @@ Proof
   Suff `((BIGUNION {Q i | i IN UNIV} INTER A) UNION (Q0 INTER A) = A) /\
                   ((BIGUNION {Q i | i IN UNIV} INTER A) INTER (Q0 INTER A) = {})` THENL
   [DISCH_TAC,
-   CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC [disjoint_family, disjoint_family_on]] THEN
+   CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC [disjoint_family_on]] THEN
    UNDISCH_TAC ``Q0 = m_space M DIFF BIGUNION {Q i | i IN univ(:num)}`` THEN
    UNDISCH_TAC ``disjoint_family (Q:num->'a->bool)`` THEN
-   SIMP_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] THEN
+   SIMP_TAC std_ss [disjoint_family_on, IN_UNIV] THEN
    FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_alt_pow, POW_DEF] THEN
    ASM_SET_TAC []] THEN
   ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN ASM_REWRITE_TAC [] THEN
@@ -10617,7 +10617,7 @@ Theorem ext_suminf_cmult_indicator :
     !A f x i. disjoint_family A /\ x IN A i /\ (!i. 0 <= f i) ==>
               (suminf (\n. f n * indicator_fn (A n) x) = f i)
 Proof
-  RW_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] THEN
+  RW_TAC std_ss [disjoint_family_on, IN_UNIV] THEN
   Suff `!n. f n * indicator_fn (A n) x = if n = i then f n else 0` THENL
   [DISCH_TAC,
    RW_TAC std_ss [indicator_fn_def, mul_rone, mul_rzero] THEN
@@ -10921,7 +10921,7 @@ Proof
                suminf (\j. indicator_fn (A j) x)`
      >- (GEN_TAC >> ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
          MATCH_MP_TAC indicator_fn_suminf \\
-         FULL_SIMP_TAC std_ss [disjoint_family, disjoint_family_on, DISJOINT_DEF] \\
+         FULL_SIMP_TAC std_ss [disjoint_family_on, DISJOINT_DEF] \\
          ASM_SET_TAC []) \\
      DISCH_TAC >> ASM_SIMP_TAC std_ss [] \\
      Know `!x. h x * suminf (\j. indicator_fn (A j) x) =
@@ -11247,26 +11247,45 @@ Proof
     simp[]
 QED
 
-Theorem integral_sum':
+(* NOTE: reworked proof for "HOL warning: Type.mk_vartype: non-standard syntax" *)
+Theorem integral_sum' :
     !m f s. FINITE s /\ measure_space m /\ (!i. i IN s ==> integrable m (f i)) ==>
-        integral m (λx. SIGMA (λi. f i x) s) = SIGMA (λi. integral m (f i)) s
+            integral m (λx. SIGMA (λi. f i x) s) = SIGMA (λi. integral m (f i)) s
 Proof
-    rw[] >>
-    resolve_then Any (resolve_then (Pos $ el 2)
-        (qspecl_then [‘zzz’,‘xxx’,‘s’,‘m’,‘λi. Normal o real o f i’] irule) integral_sum) EQ_TRANS EQ_TRANS >>
-    qexistsl_tac [‘f’,‘m’,‘s’] >> simp[] >>
-    first_assum $ C (resolve_then Any assume_tac) integrable_AE_finite >> rfs[] >>
-    qspecl_then [‘m’,‘λi x. f i x = Normal (real (f i x))’,‘s’] assume_tac AE_BIGINTER >>
-    rfs[finite_countable] >> rw[]
-    >- (irule integrable_eq_AE_alt >> simp[integrable_measurable,IN_MEASURABLE_BOREL_NORMAL_REAL] >>
-        qexists_tac ‘f i’ >> simp[])
-    >- (irule integral_cong_AE >> simp[] >>
-        qspecl_then [‘m’,‘λx. !n. n IN s ==> f n x = Normal (real (f n x))’,
-            ‘λx. SIGMA (λi. f i x) s = SIGMA (λi. Normal (real (f i x))) s’]
-            (irule o SIMP_RULE (srw_ss ()) []) AE_subset >>
-        rw[] >> irule EXTREAL_SUM_IMAGE_EQ' >> simp[])
-    >- (irule EXTREAL_SUM_IMAGE_EQ' >> simp[] >>
-        rw[] >> irule integral_cong_AE >> simp[Once EQ_SYM_EQ])
+    rpt STRIP_TAC
+ (* applying integral_sum *)
+ >> MP_TAC (Q.SPECL [‘m’, ‘\i. Normal o real o f i’, ‘s’] integral_sum)
+ >> simp []
+ >> qabbrev_tac ‘g = \i. Normal o real o f i’ >> simp []
+ >> Know ‘!i. i IN s ==> integrable m (g i)’
+ >- (rw [Abbr ‘g’] \\
+     MATCH_MP_TAC integrable_eq_AE_alt \\
+     Q.EXISTS_TAC ‘f i’ >> ASM_SIMP_TAC bool_ss [] \\
+     CONJ_TAC >- (MATCH_MP_TAC integrable_AE_finite >> rw []) \\
+     MATCH_MP_TAC IN_MEASURABLE_BOREL_NORMAL_REAL \\
+     fs [measure_space_def, integrable_def])
+ >> RW_TAC std_ss []
+ (* rewrite RHS from f to g *)
+ >> MATCH_MP_TAC EQ_TRANS
+ >> Q.EXISTS_TAC ‘SIGMA (\i. integral m (g i)) s’
+ >> reverse CONJ_TAC
+ >- (irule EXTREAL_SUM_IMAGE_EQ' >> rw [] \\
+     ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
+     MATCH_MP_TAC integral_cong_AE >> RW_TAC bool_ss [Abbr ‘g’] \\
+     MATCH_MP_TAC integrable_AE_finite >> rw [])
+ (* rewrite LHS from f to g *)
+ >> MATCH_MP_TAC EQ_TRANS
+ >> Q.EXISTS_TAC ‘integral m (\x. SIGMA (\i. g i x) s)’
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC integral_cong_AE >> rw [] \\
+     HO_MATCH_MP_TAC AE_subset \\
+     Q.EXISTS_TAC ‘\x. !i. i IN s ==> f i x = g i x’ >> simp [] \\
+     reverse CONJ_TAC >- (rpt STRIP_TAC \\
+                          irule EXTREAL_SUM_IMAGE_EQ' >> rw []) \\
+     HO_MATCH_MP_TAC AE_BIGINTER \\
+     RW_TAC bool_ss [finite_countable, Abbr ‘g’] \\
+     MATCH_MP_TAC integrable_AE_finite >> rw [])
+ >> simp [Abbr ‘g’]
 QED
 
 Theorem integrable_sum':
diff --git a/src/probability/martingaleScript.sml b/src/probability/martingaleScript.sml
index f272aaa29f..6fa6459bd8 100644
--- a/src/probability/martingaleScript.sml
+++ b/src/probability/martingaleScript.sml
@@ -6151,6 +6151,43 @@ val INFTY_SIGMA_ALGEBRA_MAXIMAL = store_thm
      Q.EXISTS_TAC `n` >> art [])
  >> REWRITE_TAC [SIGMA_SUBSET_SUBSETS]);
 
+(* A construction of sigma-filteration from only measurable functions *)
+Theorem filtration_from_measurable_functions :
+    !m X A. measure_space m /\
+           (!n. X n IN Borel_measurable (measurable_space m)) /\
+           (!n. A n = sigma (m_space m) (\n. Borel) X (count1 n)) ==>
+            filtration (measurable_space m) A
+Proof
+    rw [filtration_def]
+ >- (rw [sub_sigma_algebra_def, space_sigma_functions]
+     >- (MATCH_MP_TAC sigma_algebra_sigma_functions \\
+         rw [IN_FUNSET, SPACE_BOREL]) \\
+     MATCH_MP_TAC (REWRITE_RULE [space_def, subsets_def]
+                    (Q.ISPECL [‘measurable_space m’, ‘\n:num. Borel’]
+                               sigma_functions_subset)) \\
+     rw [MEASURE_SPACE_SIGMA_ALGEBRA, SIGMA_ALGEBRA_BOREL])
+ (* stage work *)
+ >> REWRITE_TAC [Once sigma_functions_def]
+ >> Q.ABBREV_TAC ‘B = (sigma (m_space m) (\n. Borel) X (count1 j))’
+ >> ‘m_space m = space B’ by METIS_TAC [space_sigma_functions]
+ >> POP_ORW
+ >> MATCH_MP_TAC SIGMA_SUBSET
+ >> CONJ_ASM1_TAC
+ >- (Q.UNABBREV_TAC ‘B’ \\
+     MATCH_MP_TAC sigma_algebra_sigma_functions \\
+     rw [IN_FUNSET, SPACE_BOREL])
+ >> rw [SUBSET_DEF, IN_BIGUNION_IMAGE]
+ >> rename1 ‘k < SUC i’
+ >> rename1 ‘t IN subsets Borel’
+ >> ‘k <= i’ by rw []
+ >> ‘k <= j’ by rw []
+ (* applying SIGMA_SIMULTANEOUSLY_MEASURABLE *)
+ >> Suff ‘X k IN measurable B Borel’ >- rw [IN_MEASURABLE]
+ >> MP_TAC (ISPECL [“m_space m”, “\n:num. Borel”, “X :num->'a->extreal”, “count1 j”]
+                   SIGMA_SIMULTANEOUSLY_MEASURABLE)
+ >> rw [SIGMA_ALGEBRA_BOREL, IN_FUNSET, SPACE_BOREL]
+QED
+
 (* ------------------------------------------------------------------------- *)
 (*  Martingale alternative definitions and properties (Chapter 23 of [1])    *)
 (* ------------------------------------------------------------------------- *)
diff --git a/src/probability/measureScript.sml b/src/probability/measureScript.sml
index 04ee3ab5ae..ab0c1cc97e 100644
--- a/src/probability/measureScript.sml
+++ b/src/probability/measureScript.sml
@@ -1757,7 +1757,7 @@ Theorem has_exhausting_sequence_alt =
 
    The new definition based on ‘exhausting_sequence’ (was in martingaleTheory):
  *)
-Definition sigma_finite_def0 :
+Definition sigma_finite :
     sigma_finite m = ?f. exhausting_sequence (m_space m,measurable_sets m) f /\
                          !n. measure m (f n) < PosInf
 End
@@ -1772,7 +1772,7 @@ Theorem sigma_finite_def :
            (BIGUNION (IMAGE f UNIV) = m_space m) /\
            (!n. measure m (f n) < PosInf)
 Proof
-    rw [sigma_finite_def0, exhausting_sequence_def]
+    rw [sigma_finite, exhausting_sequence_def]
  >> METIS_TAC []
 QED
 
@@ -2957,10 +2957,10 @@ val OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE = store_thm
  >> ASM_REWRITE_TAC []);
 
 (* cf. MEASURE_SPACE_RESTRICTED *)
-val MEASURE_SPACE_RESTRICTION = store_thm
-  ("MEASURE_SPACE_RESTRICTION",
-  ``!sp sts m sub. measure_space (sp,sts,m) /\ sub SUBSET sts /\ sigma_algebra (sp,sub) ==>
-                   measure_space (sp,sub,m)``,
+Theorem MEASURE_SPACE_RESTRICTION :
+    !sp sts m sub. measure_space (sp,sts,m) /\ sub SUBSET sts /\ sigma_algebra (sp,sub) ==>
+                   measure_space (sp,sub,m)
+Proof
     RW_TAC std_ss [measure_space_def, m_space_def, measurable_sets_def]
  >- (REWRITE_TAC [positive_def, measure_def, measurable_sets_def] \\
      CONJ_TAC >- PROVE_TAC [positive_def, measure_def, measurable_sets_def] \\
@@ -2969,7 +2969,22 @@ val MEASURE_SPACE_RESTRICTION = store_thm
  >> fs [countably_additive_def, IN_FUNSET, IN_UNIV, measurable_sets_def, measure_def]
  >> RW_TAC std_ss []
  >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
- >> PROVE_TAC [SUBSET_DEF]);
+ >> PROVE_TAC [SUBSET_DEF]
+QED
+
+(* Any sub-sigma-algebra in a measurable space forms a measurable space
+   cf. martingaleTheory.measure_space_from_sub_sigma_algebra
+ *)
+Theorem MEASURE_SPACE_RESTRICTION':
+   !m sts. measure_space m /\ sts SUBSET (measurable_sets m) /\
+           sigma_algebra (m_space m,sts) ==>
+           measure_space (m_space m,sts,measure m)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC MEASURE_SPACE_RESTRICTION
+ >> Q.EXISTS_TAC ‘measurable_sets m’
+ >> rw [MEASURE_SPACE_REDUCE]
+QED
 
 (* Theorem 18.2 of [1]. Given (sp,sts,m) and u = outer_measure m (countable_covers sts):
 
@@ -3921,7 +3936,7 @@ Proof
  >> `!n. FINITE (g n)`   by PROVE_TAC []
  >> `!n. disjoint (g n)` by PROVE_TAC []
  >> Q.PAT_X_ASSUM `!x. (f x = BIGUNION (g x)) /\ P` K_TAC
- (* applying countable_disjoint_decomposition *)
+ (* applying finite_disjoint_decomposition' *)
  >> Know `!x. ?h n. (!i. i < n ==> h i IN (g x)) /\ (!i. n <= i ==> (h i = {})) /\
                     (g x = IMAGE h (count n)) /\
                     (BIGUNION (g x) = BIGUNION (IMAGE h univ(:num))) /\
@@ -3929,7 +3944,7 @@ Proof
                     (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (h i) (h j))`
  >- (Q.X_GEN_TAC `n` \\
      Know `FINITE (g n) /\ disjoint (g n)` >- PROVE_TAC [] \\
-     DISCH_THEN (STRIP_ASSUME_TAC o (MATCH_MP countable_disjoint_decomposition)) \\
+     DISCH_THEN (STRIP_ASSUME_TAC o (MATCH_MP finite_disjoint_decomposition')) \\
      Q.EXISTS_TAC `f'` >> Q.EXISTS_TAC `n'` >> art [])
  >> SIMP_TAC std_ss [SKOLEM_THM] >> STRIP_TAC (* skolemization here *)
  >> `!n i. i < f'' n ==> f' n i IN g n` by PROVE_TAC []
@@ -4716,7 +4731,7 @@ Proof
  (* applying UNIQUENESS_OF_MEASURE *)
  >> Know ‘!s. s IN subsets (sigma sp sts) ==> v s = v'' s’
  >- (‘!s. s IN sts ==> v s = v'' s’ by METIS_TAC [] \\
-     MATCH_MP_TAC UNIQUENESS_OF_MEASURE >> simp [sigma_finite_def0] \\
+     MATCH_MP_TAC UNIQUENESS_OF_MEASURE >> simp [sigma_finite] \\
      fs [semiring_def, has_exhausting_sequence] \\
      CONJ_TAC >- (Q.EXISTS_TAC ‘f’ >> art [] \\
                   fs [exhausting_sequence_def, IN_FUNSET]) \\
@@ -4979,6 +4994,12 @@ Proof
  >> FIRST_X_ASSUM irule >> Q.EXISTS_TAC ‘t’ >> art []
 QED
 
+Theorem COMPLETION_STABLE' :
+    !m. complete_measure_space m ==> completion m = measurable_space m
+Proof
+    PROVE_TAC [SPACE, COMPLETION_STABLE]
+QED
+
 (* ------------------------------------------------------------------------- *)
 (*  Alternative definitions of `sigma_finite`                                *)
 (* ------------------------------------------------------------------------- *)
@@ -5032,12 +5053,12 @@ val SIGMA_FINITE_ALT = store_thm (* was: sigma_finite (HVG) *)
  >> CONJ_TAC >- REWRITE_TAC [FINITE_COUNT]
  >> RW_TAC std_ss [o_DEF, lt_infty]);
 
-val SIGMA_FINITE_ALT2 = store_thm (* was: sigma_finite_measure (HVG) *)
-  ("SIGMA_FINITE_ALT2",
-  ``!m. measure_space m ==>
+Theorem SIGMA_FINITE_ALT2 : (* was: sigma_finite_measure (HVG) *)
+    !m. measure_space m ==>
        (sigma_finite m <=> ?A. countable A /\ A SUBSET measurable_sets m /\
                               (BIGUNION A = m_space m) /\
-                              (!a. a IN A ==> measure m a <> PosInf))``,
+                              (!a. a IN A ==> measure m a <> PosInf))
+Proof
     GEN_TAC >> DISCH_TAC
  >> EQ_TAC >> rpt STRIP_TAC
  >- (fs [sigma_finite_def] \\
@@ -5069,9 +5090,11 @@ val SIGMA_FINITE_ALT2 = store_thm (* was: sigma_finite_measure (HVG) *)
       GEN_TAC >> REWRITE_TAC [GSYM lt_infty] \\
       FIRST_X_ASSUM MATCH_MP_TAC \\
       REWRITE_TAC [IN_IMAGE, IN_UNIV] \\
-      Q.EXISTS_TAC `n` >> REWRITE_TAC [] ]);
+      Q.EXISTS_TAC `n` >> REWRITE_TAC [] ]
+QED
 
-Theorem sigma_finite :
+(* NOTE: was ‘sigma_finite’ (name conflicted with its original definition) *)
+Theorem sigma_finite_thm :
     !m. measure_space m /\ sigma_finite m ==>
         ?A. IMAGE A UNIV SUBSET measurable_sets m /\
             (BIGUNION {A i | i IN UNIV} = m_space m) /\
@@ -5103,7 +5126,7 @@ Proof
     RW_TAC std_ss []
  >> `?A. IMAGE A univ(:num) SUBSET measurable_sets m /\
        (BIGUNION {A i | i IN univ(:num)} = m_space m) /\
-       !i. measure m (A i) <> PosInf` by METIS_TAC [sigma_finite]
+       !i. measure m (A i) <> PosInf` by METIS_TAC [sigma_finite_thm]
  >> Know `!i. measure m (disjointed A i) <= measure m (A i)`
  >- (GEN_TAC THEN
      MATCH_MP_TAC INCREASING THEN SIMP_TAC std_ss [disjointed_subset] \\
@@ -5196,7 +5219,7 @@ val lemma1 = prove (
 
 val lemma2 = prove (
   ``!A. (!m n. m <> n ==> DISJOINT (A m) (A n)) <=> disjoint_family A``,
-  STRIP_TAC THEN SIMP_TAC std_ss [disjoint_family, disjoint_family_on] THEN
+  STRIP_TAC THEN SIMP_TAC std_ss [disjoint_family_on] THEN
   SET_TAC []);
 
 val lemma3 = prove (
@@ -5355,12 +5378,11 @@ val measure_liminf = store_thm
       FIRST_X_ASSUM MATCH_MP_TAC \\
       Q.EXISTS_TAC `n'` >> RW_TAC arith_ss [] ]);
 
-(* An extended version of `limsup_suminf_indicator` with spaces (moved from borelTheory) *)
-val limsup_suminf_indicator_space = store_thm
-  ("limsup_suminf_indicator_space",
-  ``!a A. sigma_algebra a /\ (!n. A n IN subsets a) ==>
-         (limsup A = {x | x IN space a /\ (suminf (\n. indicator_fn (A n) x) = PosInf)})``,
- (* proof *)
+(* An extended version of `limsup_suminf_indicator` (now removed) with spaces *)
+Theorem limsup_suminf_indicator_space :
+    !a A. sigma_algebra a /\ (!n. A n IN subsets a) ==>
+         (limsup A = {x | x IN space a /\ (suminf (\n. indicator_fn (A n) x) = PosInf)})
+Proof
     RW_TAC std_ss [EXTENSION, IN_LIMSUP, GSPECIFICATION, indicator_fn_def]
  >> `(?N. INFINITE N /\ !n. n IN N ==> x IN A n) = ~(?m. !n. m <= n ==> x NOTIN A n)`
      by METIS_TAC [Q.SPEC `\n. x IN A n` infinitely_often_lemma]
@@ -5431,7 +5453,8 @@ val limsup_suminf_indicator_space = store_thm
           RW_TAC arith_ss [SUBSET_DEF, IN_COUNT, GSPECIFICATION]) \\
       DISCH_THEN (STRIP_ASSUME_TAC o (Q.SPEC `n`)) \\
       Q.EXISTS_TAC `n'` \\
-      MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `&n` >> art [] ]);
+      MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `&n` >> art [] ]
+QED
 
 (***********************)
 (*   Further Results   *)
diff --git a/src/probability/probabilityScript.sml b/src/probability/probabilityScript.sml
index fa3b599d28..6b58e8ec19 100644
--- a/src/probability/probabilityScript.sml
+++ b/src/probability/probabilityScript.sml
@@ -5401,7 +5401,7 @@ val _ = Datatype `convergence_mode = almost_everywhere   ('a p_space)
 (* convergence of extreal-valued random series [1, p.68,70], only works
    for real-valued random variables (cf. real_random_variable_def)
  *)
-Definition converge_def :
+Definition converge_def[nocompute] :
    (* X(n) converges to Y (a.e.) *)
    (converge (X :num->'a->extreal) (Y :'a->extreal) (almost_everywhere p) =
      AE x::p. ((\n. real (X n x)) --> real (Y x)) sequentially) /\
diff --git a/src/probability/sigma_algebraScript.sml b/src/probability/sigma_algebraScript.sml
index 70d31bbf38..fa1af71e95 100644
--- a/src/probability/sigma_algebraScript.sml
+++ b/src/probability/sigma_algebraScript.sml
@@ -2,8 +2,7 @@
 (* The (shared) theory of sigma-algebra and other systems of sets (ring,     *)
 (* semiring, and dynkin system) used in measureTheory/real_measureTheory     *)
 (*                                                                           *)
-(* Author: Chun Tian (2018-2020)                                             *)
-(* Fondazione Bruno Kessler and University of Trento, Italy                  *)
+(* Author: Chun Tian (2018 - 2023)                                           *)
 (* ------------------------------------------------------------------------- *)
 (* Based on the work of Tarek Mhamdi, Osman Hasan, Sofiene Tahar [3]         *)
 (* HVG Group, Concordia University, Montreal (2013, 2015)                    *)
@@ -3224,10 +3223,36 @@ QED
 (* ------------------------------------------------------------------------- *)
 
 (* The smallest sigma-algebra on `sp` that makes `f` measurable *)
-val sigma_function_def = Define
-   `sigma_function sp A f = (sp,IMAGE (\s. PREIMAGE f s INTER sp) (subsets A))`;
+Definition sigma_function_def :
+    sigma_function sp A f = (sp,IMAGE (\s. PREIMAGE f s INTER sp) (subsets A))
+End
+
+Overload sigma = “sigma_function”
+
+Theorem space_sigma_function :
+    !sp A f. space (sigma_function sp A f) = sp
+Proof
+    rw [sigma_function_def]
+QED
 
-val _ = overload_on ("sigma", ``sigma_function``);
+(* For ‘sigma_function sp A f’ to be a sigma_algebra, A must be sigma_algebra *)
+Theorem sigma_algebra_sigma_function :
+    !sp A f. sigma_algebra A /\ f IN (sp -> space A) ==>
+             sigma_algebra (sigma_function sp A f)
+Proof
+    rw [sigma_function_def]
+ >> MATCH_MP_TAC PREIMAGE_SIGMA_ALGEBRA >> art []
+QED
+
+Theorem sigma_function_subset :
+   !A B f. sigma_algebra A /\ f IN measurable A B ==>
+           subsets (sigma (space A) B f) SUBSET subsets A
+Proof
+    rw [sigma_function_def]
+ >> rw [SUBSET_DEF]
+ >> rename1 ‘t IN subsets B’
+ >> FULL_SIMP_TAC std_ss [IN_MEASURABLE]
+QED
 
 Theorem SIGMA_MEASURABLE :
     !sp A f. sigma_algebra A /\ f IN (sp -> space A) ==>
@@ -3239,13 +3264,81 @@ Proof
 QED
 
 (* Definition 7.5 of [7, p.51], The smallest sigma-algebra on `sp` that makes all `f`
-   simultaneously measurable. *)
-val sigma_functions_def = Define
-   `sigma_functions sp A f (J :'index set) =
+   simultaneously measurable.
+ *)
+Definition sigma_functions_def :
+    sigma_functions sp A f (J :'index set) =
       sigma sp (BIGUNION (IMAGE (\i. IMAGE (\s. PREIMAGE (f i) s INTER sp)
-                                           (subsets (A i))) J))`;
+                                           (subsets (A i))) J))
+End
 
-val _ = overload_on ("sigma", ``sigma_functions``);
+Overload sigma = “sigma_functions”
+
+Theorem space_sigma_functions :
+    !sp A f (J :'index set). space (sigma_functions sp A f J) = sp
+Proof
+    rw [sigma_functions_def, SPACE_SIGMA]
+QED
+
+Theorem sigma_algebra_sigma_functions :
+    !sp A f (J :'index set).
+            (!i. f i IN (sp -> space (A i))) ==>
+            sigma_algebra (sigma_functions sp A f J)
+Proof
+    rw [sigma_functions_def, IN_FUNSET]
+ >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA
+ >> rw [subset_class_def, IN_BIGUNION_IMAGE]
+ >> rw [PREIMAGE_def]
+QED
+
+(* The sigma algebra generated from A/B-measurable functions does not exceed A *)
+Theorem sigma_functions_subset :
+    !A B f (J :'index set). sigma_algebra A /\
+            (!i. i IN J ==> sigma_algebra (B i)) /\
+            (!i. i IN J ==> f i IN measurable A (B i)) ==>
+            subsets (sigma (space A) B f J) SUBSET subsets A
+Proof
+    rw [sigma_functions_def]
+ >> MATCH_MP_TAC SIGMA_SUBSET >> art []
+ >> rw [SUBSET_DEF, IN_BIGUNION_IMAGE]
+ >> rename1 ‘t IN subsets (B i)’
+ >> Q.PAT_X_ASSUM ‘!i. i IN J ==> f i IN measurable A (B n)’ (MP_TAC o (Q.SPEC ‘i’))
+ >> rw [IN_MEASURABLE]
+QED
+
+(* ‘sigma_functions’ reduce to ‘sigma_function’ when there's only one function *)
+Theorem sigma_functions_1 :
+    !sp A f. sigma_algebra A /\ f 0 IN (sp -> space A) ==>
+             sigma sp (\n. A) f (count 1) = sigma sp A (f 0)
+Proof
+    rw [sigma_functions_def]
+ >> Know ‘BIGUNION
+            (IMAGE (\n. IMAGE (\s. PREIMAGE (f n) s INTER sp) (subsets A)) (count 1)) =
+          IMAGE (\s. PREIMAGE (f 0) s INTER sp) (subsets A)’
+ >- rw [Once EXTENSION, IN_BIGUNION_IMAGE]
+ >> Rewr'
+ >> Know ‘IMAGE (\s. PREIMAGE (f 0) s INTER sp) (subsets A) =
+          subsets (sigma sp A (f 0))’
+ >- rw [sigma_function_def]
+ >> Rewr'
+ >> Q.ABBREV_TAC ‘B = sigma sp A (f 0)’
+ >> ‘sp = space B’ by METIS_TAC [space_sigma_function] >> POP_ORW
+ >> MATCH_MP_TAC SIGMA_STABLE
+ >> Q.UNABBREV_TAC ‘B’
+ >> MATCH_MP_TAC sigma_algebra_sigma_function >> art []
+QED
+
+Theorem sigma_function_alt_sigma_functions :
+    !sp A X. sigma_algebra A /\ X IN (sp -> space A) ==>
+             sigma sp A X = sigma sp (\n. A) (\n x. X x) (count 1)
+Proof
+    rpt STRIP_TAC
+ >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
+ >> Q.ABBREV_TAC ‘f = \n:num x. X x’
+ >> ‘X = f 0’ by METIS_TAC [] >> POP_ORW
+ >> MATCH_MP_TAC sigma_functions_1
+ >> rw [Abbr ‘f’, ETA_THM]
+QED
 
 (* Lemma 7.5 of [7, p.51] *)
 Theorem SIGMA_SIMULTANEOUSLY_MEASURABLE :
@@ -3789,6 +3882,30 @@ Proof
     irule MEASURABLE_PROD_SIGMA' >> simp[o_DEF,ETA_AX]
 QED
 
+Theorem algebra_finite_subsets_imp_sigma_algebra :
+    !a. algebra a /\ FINITE (subsets a) ==> sigma_algebra a
+Proof
+    rw [sigma_algebra_def]
+ >> ‘FINITE c’ by PROVE_TAC [SUBSET_FINITE_I]
+ >> MP_TAC (Q.ISPEC ‘c :('a set) set’ finite_decomposition_simple) >> rw []
+ >> MATCH_MP_TAC ALGEBRA_FINITE_UNION >> art []
+QED
+
+Theorem algebra_finite_space_imp_sigma_algebra :
+    !a. algebra a /\ FINITE (space a) ==> sigma_algebra a
+Proof
+    rw [sigma_algebra_def]
+ >> Know ‘subsets a SUBSET (POW (space a))’
+ >- (rw [Once SUBSET_DEF, IN_POW] \\
+     fs [algebra_def, subset_class_def])
+ >> DISCH_TAC
+ >> ‘FINITE (POW (space a))’ by PROVE_TAC [FINITE_POW]
+ >> ‘c SUBSET (POW (space a))’ by PROVE_TAC [SUBSET_TRANS]
+ >> ‘FINITE c’ by PROVE_TAC [SUBSET_FINITE_I]
+ >> MP_TAC (Q.ISPEC ‘c :('a set) set’ finite_decomposition_simple) >> rw []
+ >> MATCH_MP_TAC ALGEBRA_FINITE_UNION >> art []
+QED
+
 val _ = export_theory ();
 
 (* References:
diff --git a/src/probability/util_probScript.sml b/src/probability/util_probScript.sml
index daf52af879..1d93e71388 100644
--- a/src/probability/util_probScript.sml
+++ b/src/probability/util_probScript.sml
@@ -54,12 +54,12 @@ QED
 
 (********************************************************************************************)
 
-val finite_enumeration_of_sets_has_max_non_empty = store_thm
-  ("finite_enumeration_of_sets_has_max_non_empty",
-   ``!f s. FINITE s /\ (!x. f x IN s) /\
+Theorem finite_enumeration_of_sets_has_max_non_empty :
+    !f s. FINITE s /\ (!x. f x IN s) /\
             (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==>
-            ?N. !n:num. n >= N ==> (f n = {})``,
-        `!s. FINITE s ==>
+            ?N. !n:num. n >= N ==> (f n = {})
+Proof
+   `!s. FINITE s ==>
         (\s. !f. (!x. f x IN {} INSERT s) /\
                  (~({} IN s)) /\
                  (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==>
@@ -119,7 +119,8 @@ val finite_enumeration_of_sets_has_max_non_empty = store_thm
    >> Cases_on `{} IN s`
    >- (Q.PAT_X_ASSUM `!s. FINITE s ==> P` (MP_TAC o Q.SPEC `s DELETE {}`)
        >> RW_TAC std_ss [FINITE_DELETE, IN_INSERT, IN_DELETE])
-   >> METIS_TAC [IN_INSERT]);
+   >> METIS_TAC [IN_INSERT]
+QED
 
 val PREIMAGE_REAL_COMPL1 = store_thm
   ("PREIMAGE_REAL_COMPL1", ``!c:real. COMPL {x | c < x} = {x | x <= c}``,
@@ -529,11 +530,11 @@ val finite_decomposition_simple = store_thm (* new *)
  >> PROVE_TAC [BIJ_IMAGE]);
 
 (* any finite set can be decomposed into a finite (non-repeated) sequence of sets *)
-val finite_decomposition = store_thm (* new *)
-  ("finite_decomposition",
-  ``!c. FINITE c ==>
+Theorem finite_decomposition :
+    !c. FINITE c ==>
         ?f n. (!x. x < n ==> f x IN c) /\ (c = IMAGE f (count n)) /\
-              (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j)``,
+              (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j)
+Proof
     GEN_TAC
  >> REWRITE_TAC [FINITE_BIJ_COUNT_EQ]
  >> rpt STRIP_TAC
@@ -544,16 +545,17 @@ val finite_decomposition = store_thm (* new *)
  >> CONJ_TAC >- PROVE_TAC [BIJ_IMAGE]
  >> rpt STRIP_TAC
  >> fs [BIJ_ALT, IN_FUNSET, IN_COUNT]
- >> METIS_TAC []);
+ >> METIS_TAC []
+QED
 
 (* any finite disjoint set can be decomposed into a finite pair-wise
    disjoint sequence of sets *)
-val finite_disjoint_decomposition = store_thm (* new *)
-  ("finite_disjoint_decomposition",
-  ``!c. FINITE c /\ disjoint c ==>
+Theorem finite_disjoint_decomposition :
+    !c. FINITE c /\ disjoint c ==>
         ?f n. (!i. i < n ==> f i IN c) /\ (c = IMAGE f (count n)) /\
               (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j) /\
-              (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))``,
+              (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))
+Proof
     GEN_TAC
  >> REWRITE_TAC [FINITE_BIJ_COUNT_EQ]
  >> rpt STRIP_TAC
@@ -570,16 +572,18 @@ val finite_disjoint_decomposition = store_thm (* new *)
  >> rpt STRIP_TAC
  >> fs [disjoint_def]
  >> FIRST_X_ASSUM MATCH_MP_TAC
- >> METIS_TAC []);
+ >> METIS_TAC []
+QED
 
-val countable_disjoint_decomposition = store_thm (* new *)
-  ("countable_disjoint_decomposition",
-  ``!c. FINITE c /\ disjoint c ==>
+(* cf. cardinalTheory. disjoint_countable_decomposition *)
+Theorem finite_disjoint_decomposition' :
+    !c. FINITE c /\ disjoint c ==>
         ?f n. (!i. i < n ==> f i IN c) /\ (!i. n <= i ==> (f i = {})) /\
               (c = IMAGE f (count n)) /\
               (BIGUNION c = BIGUNION (IMAGE f univ(:num))) /\
               (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j) /\
-              (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))``,
+              (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))
+Proof
     rpt STRIP_TAC
  >> STRIP_ASSUME_TAC
         (MATCH_MP finite_disjoint_decomposition
@@ -598,7 +602,8 @@ val countable_disjoint_decomposition = store_thm (* new *)
  >> GEN_TAC >> EQ_TAC >> rpt STRIP_TAC
  >| [ Q.EXISTS_TAC `x'` >> METIS_TAC [],
       Cases_on `i < n` >- (Q.EXISTS_TAC `i` >> METIS_TAC []) \\
-      fs [NOT_IN_EMPTY] ]);
+      fs [NOT_IN_EMPTY] ]
+QED
 
 (* any union of two sets can be decomposed into 3 disjoint unions *)
 val UNION_TO_3_DISJOINT_UNIONS = store_thm (* new *)
@@ -634,7 +639,6 @@ val BIGUNION_IMAGE_UNIV_CROSS_UNIV = store_thm
  >- (Q.PAT_X_ASSUM `!y. ?!x. y = h x` (MP_TAC o (Q.SPEC `x'`)) >> METIS_TAC [])
  >> Q.EXISTS_TAC `h x'` >> art []);
 
-
 (* ------------------------------------------------------------------------- *)
 (*  Three series of lemmas on bigunion-equivalent sequences of sets          *)
 (* ------------------------------------------------------------------------- *)
@@ -955,9 +959,10 @@ val INCREASING_TO_DISJOINT_SETS' = store_thm
 (* ------------------------------------------------------------------------- *)
 
 (* This is not more general than disjoint_def *)
-val disjoint_family_on = new_definition ("disjoint_family_on",
-  ``disjoint_family_on a s =
-      (!m n. m IN s /\ n IN s /\ (m <> n) ==> (a m INTER a n = {}))``);
+Definition disjoint_family_on :
+    disjoint_family_on a s =
+      (!m n. m IN s /\ n IN s /\ (m <> n) ==> (a m INTER a n = {}))
+End
 
 (* A new, equivalent definition based on DISJOINT *)
 Theorem disjoint_family_on_def :
@@ -967,30 +972,31 @@ Proof
     rw [DISJOINT_DEF, disjoint_family_on]
 QED
 
-val disjoint_family = new_definition ("disjoint_family",
-  ``disjoint_family A = disjoint_family_on A UNIV``);
+Overload disjoint_family = “\A. disjoint_family_on A UNIV”
 
 (* A new, equivalent definition based on DISJOINT *)
 Theorem disjoint_family_def :
     !A. disjoint_family (A :'index -> 'a set) <=>
         !i j. i <> j ==> DISJOINT (A i) (A j)
 Proof
-    rw [disjoint_family, disjoint_family_on_def]
+    rw [disjoint_family_on_def]
 QED
 
-(* This is the way to convert a family of sets into a disjoint family *)
-(* of sets, cf. SETS_TO_DISJOINT_SETS -- Chun Tian *)
-val disjointed = new_definition ("disjointed",
-  ``!A n. disjointed A n =
-          A n DIFF BIGUNION {A i | i IN {x:num | 0 <= x /\ x < n}}``);
+(* This is the way to convert a family of sets into a disjoint family
+   of sets, cf. SETS_TO_DISJOINT_SETS -- Chun Tian
+ *)
+Definition disjointed :
+    disjointed A n = A n DIFF BIGUNION {A i | i IN {x:num | 0 <= x /\ x < n}}
+End
 
 val disjointed_subset = store_thm ("disjointed_subset",
   ``!A n. disjointed A n SUBSET A n``,
   RW_TAC std_ss [disjointed] THEN ASM_SET_TAC []);
 
-val disjoint_family_disjoint = store_thm ("disjoint_family_disjoint",
-  ``!A. disjoint_family (disjointed A)``,
-  SIMP_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] THEN
+Theorem disjoint_family_disjoint :
+    !A. disjoint_family (disjointed A)
+Proof
+  SIMP_TAC std_ss [disjoint_family_on, IN_UNIV] THEN
   RW_TAC std_ss [disjointed, EXTENSION, GSPECIFICATION, IN_INTER] THEN
   SIMP_TAC std_ss [NOT_IN_EMPTY, IN_DIFF, IN_BIGUNION] THEN
   ASM_CASES_TAC ``(x NOTIN A (m:num) \/ ?s. x IN s /\ s IN {A i | i < m})`` THEN
@@ -998,7 +1004,8 @@ val disjoint_family_disjoint = store_thm ("disjoint_family_disjoint",
   ASM_CASES_TAC ``x NOTIN A (n:num)`` THEN FULL_SIMP_TAC std_ss [] THEN
   FULL_SIMP_TAC std_ss [GSPECIFICATION] THEN
   ASM_CASES_TAC ``m < n:num`` THENL [METIS_TAC [], ALL_TAC] THEN
-  `n < m:num` by ASM_SIMP_TAC arith_ss [] THEN METIS_TAC []);
+  `n < m:num` by ASM_SIMP_TAC arith_ss [] THEN METIS_TAC []
+QED
 
 val finite_UN_disjointed_eq = prove (
   ``!A n. BIGUNION {disjointed A i | i IN {x | 0 <= x /\ x < n}} =
@@ -1314,6 +1321,13 @@ Proof
     rw [Once EXTENSION, LT_SUC_LE]
 QED
 
+(* ‘count n’ re-expressed by numseg *)
+Theorem count1_numseg :
+    !n. count1 n = {0..n}
+Proof
+    rw [Once EXTENSION]
+QED
+
 val _ = export_theory ();
 
 (* References:
diff --git a/src/real/extreal_baseScript.sml b/src/real/extreal_baseScript.sml
index 5839afa1e6..f27f90618e 100644
--- a/src/real/extreal_baseScript.sml
+++ b/src/real/extreal_baseScript.sml
@@ -28,7 +28,7 @@ val _ = Unicode.unicode_version {u = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
 val _ = TeX_notation {hol = "+" ^ UTF8.chr 0x221E,
                       TeX = ("\\ensuremath{+\\infty}", 1)};
 
-val _ = TeX_notation {hol = "-" ^ UTF8.chr 0x221E,
+val _ = TeX_notation {hol = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
                       TeX = ("\\ensuremath{-\\infty}", 1)};
 
 Definition extreal_of_num_def :
diff --git a/src/real/iterateScript.sml b/src/real/iterateScript.sml
index 67b854f57f..63f6dc1601 100644
--- a/src/real/iterateScript.sml
+++ b/src/real/iterateScript.sml
@@ -1118,6 +1118,13 @@ Proof
   simp[numseg]
 QED
 
+(* ‘count n’ re-expressed by numseg *)
+Theorem COUNT_NUMSEG :
+    !n. 0 < n ==> count n = {0..n-1}
+Proof
+    rw [Once EXTENSION]
+QED
+
 Theorem FINITE_NUMSEG:
   !m n. FINITE {m..n}
 Proof