equal
deleted
inserted
replaced
44 by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) |
44 by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) |
45 |
45 |
46 lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)" |
46 lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)" |
47 by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
47 by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
48 |
48 |
49 ML_file "measurable.ML" |
49 ML_file \<open>measurable.ML\<close> |
50 |
50 |
51 attribute_setup measurable = \<open> |
51 attribute_setup measurable = \<open> |
52 Scan.lift ( |
52 Scan.lift ( |
53 (Args.add >> K true || Args.del >> K false || Scan.succeed true) -- |
53 (Args.add >> K true || Args.del >> K false || Scan.succeed true) -- |
54 Scan.optional (Args.parens ( |
54 Scan.optional (Args.parens ( |