src/HOL/Probability/Measurable.thy
changeset 53043 8cbfbeb566a4
parent 50530 6266e44b3396
child 56021 e0c9d76c2a6d
     1.1 --- a/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:28:05 2013 +0200
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:33:36 2013 +0200
     1.3 @@ -46,10 +46,24 @@
     1.4  
     1.5  ML_file "measurable.ML"
     1.6  
     1.7 -attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
     1.8 -attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
     1.9 -attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
    1.10 -method_setup measurable = {* Measurable.method *} "measurability prover"
    1.11 +attribute_setup measurable = {*
    1.12 +  Scan.lift (Scan.optional (Args.parens (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 Measurable.add_thm))
    1.15 +*} "declaration of measurability theorems"
    1.16 +
    1.17 +attribute_setup measurable_dest = {*
    1.18 +  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
    1.19 +*} "add dest rule for measurability prover"
    1.20 +
    1.21 +attribute_setup measurable_app = {*
    1.22 +  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
    1.23 +*} "add application rule for measurability prover"
    1.24 +
    1.25 +method_setup measurable = {*
    1.26 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
    1.27 +*} "measurability prover"
    1.28 +
    1.29  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.30  
    1.31  declare