src/HOL/Probability/Measurable.thy
changeset 58965 a62cdcc5344b
parent 57025 e7fd64f82876
child 59000 6eb0725503fc
     1.1 --- a/src/HOL/Probability/Measurable.thy	Tue Nov 11 00:11:11 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Tue Nov 11 08:57:46 2014 +0100
     1.3 @@ -51,9 +51,10 @@
     1.4  ML_file "measurable.ML"
     1.5  
     1.6  attribute_setup measurable = {*
     1.7 -  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
     1.8 -    Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
     1.9 -    (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
    1.10 +  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
    1.11 +    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    1.12 +      Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    1.13 +    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
    1.14  *} "declaration of measurability theorems"
    1.15  
    1.16  attribute_setup measurable_dest = {*
    1.17 @@ -70,6 +71,10 @@
    1.18  
    1.19  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.20  
    1.21 +setup {*
    1.22 +  Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of)
    1.23 +*}
    1.24 +
    1.25  declare
    1.26    measurable_compose_rev[measurable_dest]
    1.27    pred_sets1[measurable_dest]