src/HOL/Probability/Measurable.thy
changeset 59047 8d7cec9b861d
parent 59000 6eb0725503fc
child 59048 7dc8ac6f0895
     1.1 --- a/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:35:13 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:20:35 2014 +0100
     1.3 @@ -51,23 +51,23 @@
     1.4  ML_file "measurable.ML"
     1.5  
     1.6  attribute_setup measurable = {*
     1.7 -  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
     1.8 -    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
     1.9 +  Scan.lift (
    1.10 +    (Args.add >> K true || Args.del >> K false || Scan.succeed true) --
    1.11 +    Scan.optional (Args.parens (
    1.12 +      Scan.optional (Args.$$$ "raw" >> K true) false --
    1.13        Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    1.14 -    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
    1.15 +    (false, Measurable.Concrete) >>
    1.16 +    Measurable.measurable_thm_attr)
    1.17  *} "declaration of measurability theorems"
    1.18  
    1.19 -attribute_setup measurable_dest = {*
    1.20 -  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
    1.21 -*} "add dest rule for measurability prover"
    1.22 +attribute_setup measurable_dest = Measurable.dest_thm_attr
    1.23 +  "add dest rule for measurability prover"
    1.24  
    1.25 -attribute_setup measurable_app = {*
    1.26 -  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
    1.27 -*} "add application rule for measurability prover"
    1.28 +attribute_setup measurable_app = Measurable.app_thm_attr
    1.29 +  "add application rule for measurability prover"
    1.30  
    1.31 -method_setup measurable = {*
    1.32 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
    1.33 -*} "measurability prover"
    1.34 +method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
    1.35 +  "measurability prover"
    1.36  
    1.37  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.38