Fixed normal_rv_def

binghe · Oct 3, 2024 · f8c3ff1 · f8c3ff1
1 parent e994112
commit f8c3ff1
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/examples/probability/distributionScript.sml b/examples/probability/distributionScript.sml
@@ -212,14 +212,15 @@ QED
 
 Overload ext_normal_density = “\mu sig. Normal o normal_density mu sig o real”
 
-Definition normal_measure :
+Definition normal_measure_def :
     normal_measure mu sig s =
       pos_fn_integral ext_lborel (\x. ext_normal_density mu sig x * indicator_fn s x)
 End
 
-Definition normal_rv :
+Definition normal_rv_def :
     normal_rv X p mu sig <=> real_random_variable X p /\
-                             distribution p X = normal_measure mu sig
+                             !s. s IN subsets Borel ==>
+                                 distribution p X s = normal_measure mu sig s
 End
 
 val _ = export_theory ();