src/HOL/Probability/Measurable.thy
changeset 59353 f0707dc3d9aa
parent 59088 ff2bd4a14ddb
child 59361 fd5da2434be4
     1.1 --- a/src/HOL/Probability/Measurable.thy	Sun Jan 11 21:06:47 2015 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Tue Jan 13 19:10:36 2015 +0100
     1.3 @@ -63,9 +63,6 @@
     1.4  attribute_setup measurable_dest = Measurable.dest_thm_attr
     1.5    "add dest rule to measurability prover"
     1.6  
     1.7 -attribute_setup measurable_app = Measurable.app_thm_attr
     1.8 -  "add application rule to measurability prover"
     1.9 -
    1.10  attribute_setup measurable_cong = Measurable.cong_thm_attr
    1.11    "add congurence rules to measurability prover"
    1.12  
    1.13 @@ -77,9 +74,8 @@
    1.14  setup {*
    1.15    Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
    1.16  *}
    1.17 -
    1.18 +  
    1.19  declare
    1.20 -  measurable_compose_rev[measurable_dest]
    1.21    pred_sets1[measurable_dest]
    1.22    pred_sets2[measurable_dest]
    1.23    sets.sets_into_space[measurable_dest]