From 24c610347c432c411237b7772f40f7d96b39e587 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Fri, 23 Aug 2024 23:53:38 +1000 Subject: [PATCH] Fixed statements of IN_MEASURABLE_BOREL_EL --- examples/probability/stochastic_processScript.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/probability/stochastic_processScript.sml b/examples/probability/stochastic_processScript.sml index d124eaf699..e4cf81a9be 100644 --- a/examples/probability/stochastic_processScript.sml +++ b/examples/probability/stochastic_processScript.sml @@ -1143,9 +1143,9 @@ Proof >> rw [] QED -(* |- !N i. i < N ==> EL i IN Borel_measurable (sigma_lists Borel N) *) +(* |- !N i. i < N ==> EL i IN Borel_measurable (Borel_lists N) *) Theorem IN_MEASURABLE_BOREL_EL = - SRULE [SPACE_BOREL, SIGMA_ALGEBRA_BOREL, IN_FUNSET] + SRULE [SPACE_BOREL, SIGMA_ALGEBRA_BOREL, IN_FUNSET, GSYM Borel_lists_def] (ISPEC “Borel” sigma_lists_simultaneously_measurable) val _ = export_theory ();