[isabelle-dev] Sporadic build failure of HOL-Probability in 16a8991ab398

Manuel Eberl eberlm at in.tum.de
Fri Apr 28 08:47:45 CEST 2017


Hallo,

I just had a strange build failure with HOL-Probability. I executed

manuel at colosson ~/.i/etc> isabelle-dev build -d '$AFP' Random_BSTs
Euler_MacLaurin Bertrands_Postulate

and HOL-Probability failed to build:

Building HOL-Probability ...
HOL-Probability FAILED
(see also
/home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability)

(full console output and build log attached).

There is absolutely nothing in the build log that indicates an error to
me. Also, I built HOL-Probability (without -b) a few minutes before that
and it went through fine, and when I built it again a few minutes after
the failure, it also worked fine.

For completeness, the tests were executed on an up-to-date Arch Linux
with 32 GB of RAM and a completely fresh Isabelle installation; i.e. no
settings were modified except that AFP was registered as a component. In
particular, it ran in 32 bit mode.

Cheers,

Manuel
-------------- next part --------------
Building Landau_Analysis ...
Finished Landau_Analysis (0:00:29 elapsed time, 0:01:07 cpu time, factor 2.31)
Building HOL-Number_Theory ...
Finished HOL-Number_Theory (0:01:09 elapsed time, 0:03:57 cpu time, factor 3.43)
Building Lehmer ...
Finished Lehmer (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90)
Building Pratt_Certificate ...
Finished Pratt_Certificate (0:00:25 elapsed time, 0:01:05 cpu time, factor 2.57)
Building HOL-Probability ...
HOL-Probability FAILED
(see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability)
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### inverse ?a1 \<equiv> (1::?'a1) / ?a1
### Ignoring duplicate rewrite rule:
### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1)
### Ignoring duplicate rewrite rule:
### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### frontier {..?a1} \<equiv> {?a1}
### Ambiguous input (line 1868 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Z))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" X) ("_position" Z))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Z))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###         ("_position" Z)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Quick_Sort_Cost CANCELLED
Running Bertrands_Postulate ...
^[^EFinished Bertrands_Postulate (0:01:15 elapsed time, 0:02:46 cpu time, factor 2.21)
Running Euler_MacLaurin ...
Finished Euler_MacLaurin (0:00:16 elapsed time, 0:00:32 cpu time, factor 1.95)
Random_BSTs CANCELLED
Unfinished session(s): HOL-Probability, Quick_Sort_Cost, Random_BSTs
0:05:30 elapsed time, 0:14:56 cpu time, factor 2.71


-------------- next part --------------
Loading theory "HOL-Probability.Fin_Map" (required by "Probability" via "HOL-Probability.Projective_Limit")
Loading theory "HOL-Probability.Discrete_Topology" (required by "Probability")
Loading theory "HOL-Probability.Probability_Measure" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Weak_Convergence" via "HOL-Probability.Distribution_Functions")
Loading theory "HOL-Probability.Essential_Supremum" (required by "Probability")
Loading theory "HOL-Probability.Stopping_Time" (required by "Probability")
locale prob_space =
  fixes M :: "'a measure" 
  assumes "prob_space M"
instantiation
  discrete :: (type) metric_space
  dist_discrete == dist ::
    'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real
  uniformity_discrete == uniformity ::
    ('a discrete \<times> 'a discrete) filter
  open_discrete == open :: 'a discrete set \<Rightarrow> bool
locale filtration =
  fixes \<Omega> :: "'a set" 
    and F :: "'t \<Rightarrow> 'a measure" 
  assumes "filtration \<Omega> F"
### theory "HOL-Probability.Discrete_Topology"
### 0.310s elapsed time, 1.793s cpu time, 0.063s GC time
### theory "HOL-Probability.Essential_Supremum"
### 0.315s elapsed time, 1.837s cpu time, 0.063s GC time
### theory "HOL-Probability.Stopping_Time"
### 0.374s elapsed time, 2.227s cpu time, 0.147s GC time
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
locale pair_prob_space =
  fixes M1 :: "'a measure" 
    and M2 :: "'b measure" 
  assumes "pair_prob_space M1 M2"
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
instantiation
  fmap :: (type, topological_space) topological_space
  open_fmap == open :: ('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool
locale product_prob_space =
  fixes M :: "'i \<Rightarrow> 'a measure" 
    and I :: "'i set" 
  assumes "product_prob_space M"
instantiation
  fmap :: (type, metric_space) dist
  dist_fmap == dist ::
    'a \<Rightarrow>\<^sub>F 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> real
instantiation
  fmap :: (type, metric_space) uniformity_dist
  uniformity_fmap == uniformity ::
    ('a \<Rightarrow>\<^sub>F 'b \<times>
     'a \<Rightarrow>\<^sub>F 'b) filter
### Rule already declared as introduction (intro)
### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s)
instantiation
  fmap :: (type, metric_space) metric_space
locale finite_product_prob_space =
  fixes M :: "'a \<Rightarrow> 'b measure" 
    and I :: "'a set" 
  assumes "finite_product_prob_space M I"
instantiation
  fmap :: (countable, second_countable_topology) second_countable_topology
### Ignoring duplicate rewrite rule:
### \<Prod>_\<in>?A1. (1::?'a1) \<equiv> 1::?'a1
### Rule already declared as introduction (intro)
### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk>
### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M
locale function_to_finmap =
  fixes J :: "'a set" 
    and f :: "'a \<Rightarrow> 'b" 
    and f' :: "'b \<Rightarrow> 'a" 
  assumes "function_to_finmap J f f'"
### theory "HOL-Probability.Fin_Map"
### 1.297s elapsed time, 9.027s cpu time, 0.513s GC time
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### theory "HOL-Probability.Probability_Measure"
### 1.579s elapsed time, 11.077s cpu time, 0.603s GC time
Loading theory "HOL-Probability.Conditional_Expectation" (required by "Probability")
Loading theory "HOL-Probability.Distribution_Functions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Weak_Convergence")
Loading theory "HOL-Probability.Giry_Monad" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family" via "HOL-Probability.Infinite_Product_Measure" via "HOL-Probability.Projective_Family")
locale finite_borel_measure =
  fixes M :: "real measure" 
  assumes "finite_borel_measure M"
locale real_distribution =
  fixes M :: "real measure" 
  assumes "real_distribution M"
locale sigma_finite_subalgebra =
  fixes M :: "'a measure" 
    and F :: "'a measure" 
  assumes "sigma_finite_subalgebra M F"
### theory "HOL-Probability.Distribution_Functions"
### 0.364s elapsed time, 2.607s cpu time, 0.173s GC time
Loading theory "HOL-Probability.Weak_Convergence" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions")
locale finite_measure_subalgebra =
  fixes M :: "'a measure" 
    and F :: "'a measure" 
  assumes "finite_measure_subalgebra M F"
locale sigma_finite_subalgebra =
  fixes M :: "'a measure" 
    and F :: "'a measure" 
  assumes "sigma_finite_subalgebra M F"
### Metis: Unused theorems: "Set.in_mono"
locale sigma_finite_subalgebra =
  fixes M :: "'a measure" 
    and F :: "'a measure" 
  assumes "sigma_finite_subalgebra M F"
locale right_continuous_mono =
  fixes f :: "real \<Rightarrow> real" 
    and a :: "real" 
    and b :: "real" 
  assumes "right_continuous_mono f a b"
locale cdf_distribution =
  fixes M :: "real measure" 
  assumes "cdf_distribution M"
locale subprob_space =
  fixes M :: "'a measure" 
  assumes "subprob_space M"
### theory "HOL-Probability.Conditional_Expectation"
### 0.691s elapsed time, 4.937s cpu time, 0.307s GC time
### theory "HOL-Probability.Weak_Convergence"
### 0.375s elapsed time, 2.697s cpu time, 0.133s GC time
Loading theory "HOL-Probability.Helly_Selection" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy")
locale pair_subprob_space =
  fixes M1 :: "'a measure" 
    and M2 :: "'b measure" 
  assumes "pair_subprob_space M1 M2"
val subprob_cong = fn: thm -> Proof.context -> 'a list * Proof.context
### theory "HOL-Probability.Giry_Monad"
### 1.618s elapsed time, 11.497s cpu time, 0.707s GC time
Loading theory "HOL-Probability.Probability_Mass_Function" (required by "Probability" via "HOL-Probability.PMF_Impl")
Loading theory "HOL-Probability.Projective_Family" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family" via "HOL-Probability.Infinite_Product_Measure")
### theory "HOL-Probability.Helly_Selection"
### 1.089s elapsed time, 7.730s cpu time, 0.550s GC time
### Rule already declared as introduction (intro)
### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow>
### almost_everywhere ?M ?P
locale projective_family =
  fixes I :: "'i set" 
    and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" 
    and M :: "'i \<Rightarrow> 'a measure" 
  assumes "projective_family I P M"
locale pmf_as_measure
### Generation of a parametrized correspondence relation failed.
### Reason:  No relator for the type "Sigma_Algebra.measure" found.
Proofs for inductive predicate(s) "generatorp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale Ionescu_Tulcea =
  fixes
    P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure"
      
    and M :: "nat \<Rightarrow> 'a measure" 
  assumes "Ionescu_Tulcea P M"
consts
  C :: "nat
        \<Rightarrow> nat
                      \<Rightarrow> (nat \<Rightarrow> 'a)
                                    \<Rightarrow> (nat
             \<Rightarrow> 'a) measure"
### theory "HOL-Probability.Projective_Family"
### 0.815s elapsed time, 5.310s cpu time, 0.367s GC time
Loading theory "HOL-Probability.Infinite_Product_Measure" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family")
locale pmf_as_function
Proofs for inductive predicate(s) "rel_pmf"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  replicate_pmf :: "nat \<Rightarrow> 'a pmf \<Rightarrow> 'a list pmf"
### theory "HOL-Probability.Probability_Mass_Function"
### 1.643s elapsed time, 9.960s cpu time, 0.720s GC time
Loading theory "HOL-Probability.PMF_Impl" (required by "Probability")
locale sequence_space =
  fixes M :: "'a measure" 
  assumes "sequence_space M"
### theory "HOL-Probability.Infinite_Product_Measure"
### 0.935s elapsed time, 5.257s cpu time, 0.400s GC time
Loading theory "HOL-Probability.Random_Permutations" (required by "Probability")
Loading theory "HOL-Probability.SPMF" (required by "Probability")
Loading theory "HOL-Probability.Independent_Family" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions")
### theory "HOL-Probability.Random_Permutations"
### 0.871s elapsed time, 4.960s cpu time, 0.440s GC time
Loading theory "HOL-Probability.Projective_Limit" (required by "Probability")
instantiation
  pmf :: (equal) equal
  equal_pmf == equal_class.equal ::
    'a pmf \<Rightarrow> 'a pmf \<Rightarrow> bool
Loading theory "HOL-Probability.Stream_Space" (required by "Probability")
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
instantiation
  pmf :: (random) random
  random_pmf == random_class.random ::
    natural
    \<Rightarrow> natural \<times> natural
                  \<Rightarrow> ('a pmf \<times>
                                 (unit \<Rightarrow> term)) \<times>
                                natural \<times> natural
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
Proofs for inductive predicate(s) "ord_option"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
instantiation
  pmf :: (full_exhaustive) full_exhaustive
  full_exhaustive_pmf == full_exhaustive_class.full_exhaustive ::
    ('a pmf \<times> (unit \<Rightarrow> term)
     \<Rightarrow> (bool \<times> term list) option)
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option
### theory "HOL-Probability.Independent_Family"
### 1.091s elapsed time, 6.890s cpu time, 0.660s GC time
Loading theory "HOL-Probability.Convolution" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Distributions")
### theory "HOL-Probability.PMF_Impl"
### 1.783s elapsed time, 10.740s cpu time, 0.927s GC time
Loading theory "HOL-Probability.Information" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Distributions")
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
consts
  sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set"
consts
  scylinder ::
    "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
locale finmap_seqs_into_compact =
  fixes K :: "nat \<Rightarrow> (nat \<Rightarrow>\<^sub>F 'a) set" 
    and f :: "nat \<Rightarrow> nat \<Rightarrow>\<^sub>F 'a" 
    and M :: "'b" 
  assumes "finmap_seqs_into_compact K f"
### theory "HOL-Probability.Stream_Space"
### 1.039s elapsed time, 6.530s cpu time, 0.670s GC time
locale polish_projective =
  fixes I :: "'i set" 
    and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" 
  assumes "polish_projective I P"
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
locale information_space =
  fixes M :: "'a measure" 
    and b :: "real" 
  assumes "information_space M b"
locale information_space =
  fixes M :: "'a measure" 
    and b :: "real" 
  assumes "information_space M b"
### Ambiguous input (line 61 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" log)
###       ("_cargs" ("_position" b)
###         ("\<^const>Fields.inverse_class.inverse_divide" ("_position" A)
###           ("_position" B))))
###     ("\<^const>HOL.If"
###       ("\<^const>Orderings.ord_class.less"
###         ("\<^const>Groups.zero_class.zero")
###         ("\<^const>Groups.times_class.times" ("_position" A)
###           ("_position" B)))
###       ("\<^const>Groups.minus_class.minus"
###         ("_applC" ("_position" log)
###           ("_cargs" ("_position" b)
###             ("\<^const>Groups.abs_class.abs" ("_position" A))))
###         ("_applC" ("_position" log)
###           ("_cargs" ("_position" b)
###             ("\<^const>Groups.abs_class.abs" ("_position" B)))))
###       ("_applC" ("_position" log)
###         ("_cargs" ("_position" b) ("\<^const>Groups.zero_class.zero"))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" log)
###       ("_cargs" ("_position" b)
###         ("\<^const>Fields.inverse_class.inverse_divide" ("_position" A)
###           ("_position" B))))
###     ("\<^const>HOL.If"
###       ("\<^const>Orderings.ord_class.less"
###         ("\<^const>Groups.zero_class.zero")
###         ("\<^const>Groups.times_class.times" ("_position" A)
###           ("_position" B)))
###       ("_applC" ("_position" log)
###         ("_cargs" ("_position" b)
###           ("\<^const>Groups.abs_class.abs"
###             ("_applC" ("_position" A)
###               ("_cargs"
###                 ("\<^const>Groups.abs_class.abs"
###                   ("\<^const>Groups.uminus_class.uminus"
###                     ("_applC" ("_position" log) ("_position" b))))
###                 ("_position" B))))))
###       ("_applC" ("_position" log)
###         ("_cargs" ("_position" b) ("\<^const>Groups.zero_class.zero"))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "HOL-Probability.Convolution"
### 0.359s elapsed time, 2.133s cpu time, 0.230s GC time
locale polish_product_prob_space =
  fixes I :: "'i set" 
  assumes "polish_product_prob_space TYPE('a) TYPE('i)"
locale ord_spmf_syntax
### theory "HOL-Probability.Projective_Limit"
### 1.547s elapsed time, 8.750s cpu time, 0.943s GC time
### Additional type variable(s) in locale specification "rel_spmf_characterisation": 'a, 'b
locale rel_spmf_characterisation =
  assumes "rel_spmf_characterisation TYPE('a) TYPE('b)"
### Ambiguous input (line 947 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>Pure.eq"
###   ("\<^fixed>conditional_mutual_information_Pow" ("_position" X)
###     ("_position" Y) ("_position" Z))
###   ("_applC" ("_position" conditional_mutual_information)
###     ("_cargs" ("_position" b)
###       ("_cargs"
###         ("_applC" ("_position" count_space)
###           ("\<^const>Set.image" ("_position" X)
###             ("_applC" ("_position" space) ("_position" M))))
###         ("_cargs"
###           ("_applC" ("_position" count_space)
###             ("\<^const>Set.image" ("_position" Y)
###               ("_applC" ("_position" space) ("_position" M))))
###           ("_cargs"
###             ("_applC" ("_position" count_space)
###               ("\<^const>Set.image" ("_position" Z)
###                 ("_applC" ("_position" space) ("_position" M))))
###             ("_cargs" ("_position" X)
###               ("_cargs" ("_position" Y) ("_position" Z)))))))))
### ("\<^const>Pure.eq"
###   ("\<^const>local.mutual_information_Pow" ("_position" X)
###     ("\<^const>HOL.disj" ("_position" Y) ("_position" Z)))
###   ("_applC" ("_position" conditional_mutual_information)
###     ("_cargs" ("_position" b)
###       ("_cargs"
###         ("_applC" ("_position" count_space)
###           ("\<^const>Set.image" ("_position" X)
###             ("_applC" ("_position" space) ("_position" M))))
###         ("_cargs"
###           ("_applC" ("_position" count_space)
###             ("\<^const>Set.image" ("_position" Y)
###               ("_applC" ("_position" space) ("_position" M))))
###           ("_cargs"
###             ("_applC" ("_position" count_space)
###               ("\<^const>Set.image" ("_position" Z)
###                 ("_applC" ("_position" space) ("_position" M))))
###             ("_cargs" ("_position" X)
###               ("_cargs" ("_position" Y) ("_position" Z)))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ambiguous input (line 1440 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.conditional_mutual_information_Pow" ("_position" X)
###       ("_position" Y) ("_position" Z))
###     ("_sum"
###       ("_pattern" ("_position" x)
###         ("_patterns" ("_position" y) ("_position" z)))
###       ("\<^const>Set.image"
###         ("_lambda" ("_position" x)
###           ("_tuple" ("_applC" ("_position" X) ("_position" x))
###             ("_tuple_args" ("_applC" ("_position" Y) ("_position" x))
###               ("_tuple_arg" ("_applC" ("_position" Z) ("_position" x))))))
###         ("_applC" ("_position" space) ("_position" M)))
###       ("\<^const>Groups.times_class.times"
###         ("_applC" ("_position" Pxyz)
###           ("_tuple" ("_position" x)
###             ("_tuple_args" ("_position" y) ("_tuple_arg" ("_position" z)))))
###         ("_applC" ("_position" log)
###           ("_cargs" ("_position" b)
###             ("\<^const>Fields.inverse_class.inverse_divide"
###               ("_applC" ("_position" Pxyz)
###                 ("_tuple" ("_position" x)
###                   ("_tuple_args" ("_position" y)
###                     ("_tuple_arg" ("_position" z)))))
###               ("\<^const>Groups.times_class.times"
###                 ("_applC" ("_position" Pxz)
###                   ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))))
###                 ("\<^const>Fields.inverse_class.inverse_divide"
###                   ("_applC" ("_position" Pyz)
###                     ("_tuple" ("_position" y)
###                       ("_tuple_arg" ("_position" z))))
###                   ("_applC" ("_position" Pz) ("_position" z)))))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("\<^const>HOL.disj" ("_position" Y) ("_position" Z)))
###     ("_sum"
###       ("_pattern" ("_position" x)
###         ("_patterns" ("_position" y) ("_position" z)))
###       ("\<^const>Set.image"
###         ("_lambda" ("_position" x)
###           ("_tuple" ("_applC" ("_position" X) ("_position" x))
###             ("_tuple_args" ("_applC" ("_position" Y) ("_position" x))
###               ("_tuple_arg" ("_applC" ("_position" Z) ("_position" x))))))
###         ("_applC" ("_position" space) ("_position" M)))
###       ("\<^const>Groups.times_class.times"
###         ("_applC" ("_position" Pxyz)
###           ("_tuple" ("_position" x)
###             ("_tuple_args" ("_position" y) ("_tuple_arg" ("_position" z)))))
###         ("_applC" ("_position" log)
###           ("_cargs" ("_position" b)
###             ("\<^const>Fields.inverse_class.inverse_divide"
###               ("_applC" ("_position" Pxyz)
###                 ("_tuple" ("_position" x)
###                   ("_tuple_args" ("_position" y)
###                     ("_tuple_arg" ("_position" z)))))
###               ("\<^const>Groups.times_class.times"
###                 ("_applC" ("_position" Pxz)
###                   ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))))
###                 ("\<^const>Fields.inverse_class.inverse_divide"
###                   ("_applC" ("_position" Pyz)
###                     ("_tuple" ("_position" y)
###                       ("_tuple_arg" ("_position" z))))
###                   ("_applC" ("_position" Pz) ("_position" z)))))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1487 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>Groups.zero_class.zero")
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("\<^const>HOL.disj" ("_position" Y) ("_position" Z)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>Groups.zero_class.zero")
###     ("\<^const>local.conditional_mutual_information_Pow" ("_position" X)
###       ("_position" Y) ("_position" Z))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1524 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>Pure.eq"
###   ("\<^fixed>conditional_entropy_Pow" ("_position" X) ("_position" Y))
###   ("_applC" ("_position" conditional_entropy)
###     ("_cargs" ("_position" b)
###       ("_cargs"
###         ("_applC" ("_position" count_space)
###           ("\<^const>Set.image" ("_position" X)
###             ("_applC" ("_position" space) ("_position" M))))
###         ("_cargs"
###           ("_applC" ("_position" count_space)
###             ("\<^const>Set.image" ("_position" Y)
###               ("_applC" ("_position" space) ("_position" M))))
###           ("_cargs" ("_position" X) ("_position" Y)))))))
### ("\<^const>Pure.eq"
###   ("\<^const>local.entropy_Pow"
###     ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))
###   ("_applC" ("_position" conditional_entropy)
###     ("_cargs" ("_position" b)
###       ("_cargs"
###         ("_applC" ("_position" count_space)
###           ("\<^const>Set.image" ("_position" X)
###             ("_applC" ("_position" space) ("_position" M))))
###         ("_cargs"
###           ("_applC" ("_position" count_space)
###             ("\<^const>Set.image" ("_position" Y)
###               ("_applC" ("_position" space) ("_position" M))))
###           ("_cargs" ("_position" X) ("_position" Y)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1626 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Y))
###     ("\<^const>Groups.minus_class.minus"
###       ("_applC" ("_position" entropy)
###         ("_cargs" ("_position" b)
###           ("_cargs"
###             ("\<^const>Binary_Product_Measure.pair_measure"
###               ("_applC" ("_position" count_space)
###                 ("\<^const>Set.image" ("_position" X)
###                   ("_applC" ("_position" space) ("_position" M))))
###               ("_applC" ("_position" count_space)
###                 ("\<^const>Set.image" ("_position" Y)
###                   ("_applC" ("_position" space) ("_position" M)))))
###             ("_lambda" ("_position" x)
###               ("_tuple" ("_applC" ("_position" X) ("_position" x))
###                 ("_tuple_arg"
###                   ("_applC" ("_position" Y) ("_position" x))))))))
###       ("\<^const>local.entropy_Pow" ("_position" Y)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))
###     ("\<^const>Groups.minus_class.minus"
###       ("_applC" ("_position" entropy)
###         ("_cargs" ("_position" b)
###           ("_cargs"
###             ("\<^const>Binary_Product_Measure.pair_measure"
###               ("_applC" ("_position" count_space)
###                 ("\<^const>Set.image" ("_position" X)
###                   ("_applC" ("_position" space) ("_position" M))))
###               ("_applC" ("_position" count_space)
###                 ("\<^const>Set.image" ("_position" Y)
###                   ("_applC" ("_position" space) ("_position" M)))))
###             ("_lambda" ("_position" x)
###               ("_tuple" ("_applC" ("_position" X) ("_position" x))
###                 ("_tuple_arg"
###                   ("_applC" ("_position" Y) ("_position" x))))))))
###       ("\<^const>local.entropy_Pow" ("_position" Y)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1640 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Y))
###     ("\<^const>Groups.uminus_class.uminus"
###       ("_sum" ("_pattern" ("_position" x) ("_position" y))
###         ("\<^const>Set.image"
###           ("_lambda" ("_position" x)
###             ("_tuple" ("_applC" ("_position" X) ("_position" x))
###               ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x)))))
###           ("_applC" ("_position" space) ("_position" M)))
###         ("\<^const>Groups.times_class.times"
###           ("_applC" ("_position" Pxy)
###             ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y))))
###           ("_applC" ("_position" log)
###             ("_cargs" ("_position" b)
###               ("\<^const>Fields.inverse_class.inverse_divide"
###                 ("_applC" ("_position" Pxy)
###                   ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y))))
###                 ("_applC" ("_position" Py) ("_position" y))))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))
###     ("\<^const>Groups.uminus_class.uminus"
###       ("_sum" ("_pattern" ("_position" x) ("_position" y))
###         ("\<^const>Set.image"
###           ("_lambda" ("_position" x)
###             ("_tuple" ("_applC" ("_position" X) ("_position" x))
###               ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x)))))
###           ("_applC" ("_position" space) ("_position" M)))
###         ("\<^const>Groups.times_class.times"
###           ("_applC" ("_position" Pxy)
###             ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y))))
###           ("_applC" ("_position" log)
###             ("_cargs" ("_position" b)
###               ("\<^const>Fields.inverse_class.inverse_divide"
###                 ("_applC" ("_position" Pxy)
###                   ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y))))
###                 ("_applC" ("_position" Py) ("_position" y))))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1667 of "~~/src/HOL/Probability/Information.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.conditional_mutual_information_Pow" ("_position" X)
###       ("_position" X) ("_position" Y))
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.conditional_mutual_information_Pow" ("_position" X)
###       ("_position" X) ("_position" Y))
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Y))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Y))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "HOL-Probability.SPMF"
### 3.140s elapsed time, 14.943s cpu time, 1.740s GC time
### Ambiguous input (line 1709 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>Groups.zero_class.zero")
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>Groups.zero_class.zero")
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Y))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1816 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Y))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" X) ("_position" Y))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Y))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###         ("_position" Y)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1865 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###       ("_position" Z))
###     ("\<^const>local.entropy_Pow" ("_position" X))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("\<^const>local.entropy_Pow"
###       ("\<^const>HOL.disj" ("_position" X) ("_position" Z)))
###     ("\<^const>local.entropy_Pow" ("_position" X))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1894 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.entropy_Pow"
###       ("_lambda" ("_position" x)
###         ("_tuple" ("_applC" ("_position" X) ("_position" x))
###           ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x))))))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" Y) ("_position" X))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.entropy_Pow"
###       ("_lambda" ("_position" x)
###         ("_tuple" ("_applC" ("_position" X) ("_position" x))
###           ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x))))))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" Y)
###         ("_position" X)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1919 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X)))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" X)
###           ("\<^const>Fun.comp" ("_position" f) ("_position" X)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X)))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "HOL-Probability.Information"
### 2.267s elapsed time, 8.447s cpu time, 1.123s GC time
Loading theory "HOL-Probability.Distributions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions")
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### set_pmf (map_pmf ?f1 ?M1) \<equiv> ?f1 ` set_pmf ?M1
### Ignoring duplicate rewrite rule:
### \<lbrakk>\<And>i. 0 \<le> ?f1 i;
###  (\<Sum>i. ennreal (?f1 i)) \<noteq> top\<rbrakk>
### \<Longrightarrow> \<Sum>i. ennreal (?f1 i) \<equiv> ennreal (\<Sum>i. ?f1 i)
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### theory "HOL-Probability.Distributions"
### 1.507s elapsed time, 7.600s cpu time, 0.710s GC time
Loading theory "HOL-Probability.Characteristic_Functions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy")
Loading theory "HOL-Probability.Sinc_Integral" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy")
### Ignoring duplicate rewrite rule:
### (\<And>x.
###     x \<in> set ?xs1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow>
### \<Sum>x\<leftarrow>?xs1. ennreal (?f1 x) \<equiv>
### ennreal (sum_list (map ?f1 ?xs1))
### theory "HOL-Probability.Sinc_Integral"
### 0.460s elapsed time, 2.760s cpu time, 0.277s GC time
### Rule already declared as introduction (intro)
### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow>
### almost_everywhere ?M ?P
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### theory "HOL-Probability.Characteristic_Functions"
### 1.534s elapsed time, 9.127s cpu time, 0.883s GC time
Loading theory "HOL-Probability.Levy" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem")
### Ignoring duplicate safe introduction (intro!)
### (\<And>i. {x \<in> space ?M. ?P i x} \<in> sets ?M) \<Longrightarrow>
### {x \<in> space ?M. \<forall>i. ?P i x} \<in> sets ?M
### Rule already declared as introduction (intro)
### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk>
### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M
### theory "HOL-Probability.Levy"
### 1.710s elapsed time, 8.160s cpu time, 1.170s GC time
Loading theory "HOL-Probability.Central_Limit_Theorem" (required by "Probability")
### theory "HOL-Probability.Central_Limit_Theorem"
### 0.867s elapsed time, 2.913s cpu time, 0.533s GC time
Loading theory "Probability"
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?I; ?I \<noteq> {};
###  \<And>i. i \<in> ?I \<Longrightarrow> ?A i \<in> sets ?M\<rbrakk>
### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i) \<in> sets ?M
### Ignoring duplicate rewrite rule:
### (\<And>x.
###     x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow>
### (\<lambda>x. ennreal (?f1 x)) \<in> borel_measurable ?M1 \<equiv>
### ?f1 \<in> borel_measurable ?M1
### Ignoring duplicate rewrite rule:
### (\<And>x.
###     x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow>
### (\<lambda>x. ennreal (?f1 x)) \<in> borel_measurable ?M1 \<equiv>
### ?f1 \<in> borel_measurable ?M1
### Rule already declared as introduction (intro)
### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk>
### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M
### theory "Probability"
### 3.800s elapsed time, 16.140s cpu time, 3.853s GC time
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1
### Ignoring duplicate rewrite rule:
### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1
### Ignoring duplicate rewrite rule:
### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1
### Ignoring duplicate rewrite rule:
### inverse ?a1 \<equiv> (1::?'a1) / ?a1
### Ignoring duplicate rewrite rule:
### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1)
### Ignoring duplicate rewrite rule:
### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Ignoring duplicate rewrite rule:
### of_nat (?m1 * ?n1) \<equiv> of_nat ?m1 * of_nat ?n1
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1069 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("_nn_integral" ("_position" x)
###       ("\<^const>Groups.times_class.times"
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pyz) ("_position" x)))
###         ("\<^const>Groups.one_class.one"))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###         ("_position" P)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("\<^const>Groups.times_class.times"
###           ("_applC" ("_position" ennreal)
###             ("_applC" ("_position" Pyz) ("_position" x)))
###           ("\<^const>Groups.one_class.one"))
###         ("_position" T))
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Introduced fixed type variable(s): 'c in "Sa__" or "Xa__"
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1322 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("_nn_integral" ("_pattern" ("_position" y) ("_position" z))
###       ("_nn_integral" ("_position" x)
###         ("\<^const>Groups.times_class.times"
###           ("_applC" ("_position" ennreal)
###             ("_applC" ("_position" Pxz)
###               ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z)))))
###           ("_applC" ("_position" ennreal)
###             ("\<^const>Fields.inverse_class.inverse_divide"
###               ("_applC" ("_position" Pyz)
###                 ("_tuple" ("_position" y) ("_tuple_arg" ("_position" z))))
###               ("_applC" ("_position" Pz) ("_position" z)))))
###         ("_position" S))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###         ("_position" P)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_pattern" ("_position" y) ("_position" z))
###         ("_nn_integral" ("_position" x)
###           ("\<^const>Groups.times_class.times"
###             ("_applC" ("_position" ennreal)
###               ("_applC" ("_position" Pxz)
###                 ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z)))))
###             ("_applC" ("_position" ennreal)
###               ("\<^const>Fields.inverse_class.inverse_divide"
###                 ("_applC" ("_position" Pyz)
###                   ("_tuple" ("_position" y) ("_tuple_arg" ("_position" z))))
###                 ("_applC" ("_position" Pz) ("_position" z)))))
###           ("_position" S))
###         ("_position" T))
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1326 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("_nn_integral" ("_position" x)
###       ("\<^const>Groups.times_class.times"
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pyz) ("_position" x)))
###         ("\<^const>Groups.one_class.one"))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###         ("_position" P)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("\<^const>Groups.times_class.times"
###           ("_applC" ("_position" ennreal)
###             ("_applC" ("_position" Pyz) ("_position" x)))
###           ("\<^const>Groups.one_class.one"))
###         ("_position" T))
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. x) \<longlongrightarrow> ?a1) (at ?a1 within ?s1) \<equiv>
### True
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow>
### ((\<lambda>x. ereal (?f1 x)) \<longlongrightarrow> ereal ?x1) ?F1 \<equiv>
### True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow>
### ((\<lambda>x. - ?f1 x) \<longlongrightarrow> - ?x1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>\<bar>?c1\<bar> \<noteq> \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow>
###                    ?c1 * ?x1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<noteq> 0; (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow>
###                    ?c1 * ?x1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?y1 \<noteq> - \<infinity>; ?x1 \<noteq> - \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow>
###                    ?x1 + ?y1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>\<bar>?y1\<bar> \<noteq> \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow>
###                    ?x1 + ?y1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk>
### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x)
### Rule already declared as introduction (intro)
### integrable ?M ?f \<Longrightarrow>
### integrable ?M (\<lambda>x. \<bar>?f x\<bar>)
### Rule already declared as introduction (intro)
### (?c \<noteq> (0::?'b) \<Longrightarrow> integrable ?M ?f) \<Longrightarrow>
### integrable ?M (\<lambda>x. ?c * ?f x)
### Rule already declared as introduction (intro)
### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk>
### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x - ?g x)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f)
### Rule already declared as introduction (intro)
### ?A ` ?X \<subseteq> sets ?M \<Longrightarrow>
### (\<Union>x\<in>?X. ?A x) \<in> sets ?M
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow>
### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow>
### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f
### Rule already declared as introduction (intro)
### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk>
### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x)
### Rule already declared as introduction (intro)
### integrable ?M ?f \<Longrightarrow>
### integrable ?M (\<lambda>x. \<bar>?f x\<bar>)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow>
### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f
### Rule already declared as introduction (intro)
### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow>
### almost_everywhere ?M ?P
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> enn2real ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?I; ?I \<noteq> {};
###  \<And>i. i \<in> ?I \<Longrightarrow> ?A i \<in> sets ?M\<rbrakk>
### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i) \<in> sets ?M
### Ignoring duplicate rewrite rule:
### 0 \<le> enn2real ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> enn2real ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?I; ?I \<noteq> {};
###  \<And>i.
###     i \<in> ?I \<Longrightarrow>
###     ?A i \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)\<rbrakk>
### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i)
###                   \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk>
### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x)
### Rule already declared as introduction (intro)
### integrable ?M ?f \<Longrightarrow>
### integrable ?M (\<lambda>x. \<bar>?f x\<bar>)
### Rule already declared as introduction (intro)
### (?c \<noteq> (0::?'b) \<Longrightarrow> integrable ?M ?f) \<Longrightarrow>
### integrable ?M (\<lambda>x. ?c * ?f x)
### Rule already declared as introduction (intro)
### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk>
### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x - ?g x)
### Rule already declared as introduction (intro)
### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f)
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk>
### \<Longrightarrow> ?a - ?b \<in> sets ?M
### Ignoring duplicate rewrite rule:
### \<Prod>_\<in>?A1. (1::?'a1) \<equiv> 1::?'a1
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1097 of "~~/src/HOL/Probability/Information.thy") produces 3 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pxyz) ("_position" x)))
###         ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S)
###           ("_position" T)))
###       ("_position" P))
###     ("\<^const>Groups.zero_class.zero")))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_nn_integral" ("_position" x)
###       ("_applC" ("_position" ennreal)
###         ("_applC" ("_position" Pxyz) ("_position" x)))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S)
###         ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###           ("_position" P))))
###     ("\<^const>Groups.zero_class.zero")))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pxyz) ("_position" x)))
###         ("_position" S))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###         ("_position" P)))
###     ("\<^const>Groups.zero_class.zero")))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Rule already declared as introduction (intro)
### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow>
### almost_everywhere ?M ?P
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Ambiguous input (line 1358 of "~~/src/HOL/Probability/Information.thy") produces 3 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pxyz) ("_position" x)))
###         ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S)
###           ("_position" T)))
###       ("_position" P))
###     ("\<^const>Groups.zero_class.zero")))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_nn_integral" ("_position" x)
###       ("_applC" ("_position" ennreal)
###         ("_applC" ("_position" Pxyz) ("_position" x)))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S)
###         ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###           ("_position" P))))
###     ("\<^const>Groups.zero_class.zero")))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Binary_Product_Measure.pair_measure"
###       ("_nn_integral" ("_position" x)
###         ("_applC" ("_position" ennreal)
###           ("_applC" ("_position" Pxyz) ("_position" x)))
###         ("_position" S))
###       ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T)
###         ("_position" P)))
###     ("\<^const>Groups.zero_class.zero")))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### (\<And>x.
###     x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow>
### 0 \<le> integral\<^sup>L ?M1 ?f1 \<equiv> True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow>
### open (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union>?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
### continuous_on UNIV ?f
### Rule already declared as introduction (intro)
### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s)
### Rule already declared as introduction (intro)
### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F
### Rule already declared as introduction (intro)
### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F
### Rule already declared as introduction (intro)
### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### of_real (?x1 * ?y1) \<equiv> of_real ?x1 * of_real ?y1
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s)
### Rule already declared as introduction (intro)
### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F
### Rule already declared as introduction (intro)
### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F
### Rule already declared as introduction (intro)
### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
### Rule already declared as introduction (intro)
### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>;
###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
### Rule already declared as introduction (intro)
### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow>
### almost_everywhere ?M ?P
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>?A ` ?X
###          \<subseteq> sigma_sets (space M)
###                       (\<Union>i\<in>{j..}. sigma_sets (space M) {F i});
###  ?X \<noteq> {}\<rbrakk>
### \<Longrightarrow> (\<Inter>i\<in>?X. ?A i)
###                   \<in> sigma_sets (space M)
###                          (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})
### Rule already declared as introduction (intro)
### ?A ` ?X
### \<subseteq> sigma_sets (space M)
###              (\<Union>i\<in>{j..}.
###                  sigma_sets (space M) {F i}) \<Longrightarrow>
### (\<Union>x\<in>?X. ?A x)
### \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})
### Rule already declared as introduction (intro)
### ?a \<in> ?A \<Longrightarrow> ?a \<in> sigma_sets ?sp ?A
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?x; ?x \<in> ?A\<rbrakk>
### \<Longrightarrow> \<exists>x\<in>?A. ?P x
### Rule already declared as introduction (intro)
### ?a \<in> ?A \<Longrightarrow> ?a \<in> sigma_sets ?sp ?A
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
### Rule already declared as introduction (intro)
### \<lbrakk>?A \<in> sets ?M; emeasure ?M ?A < \<infinity>\<rbrakk>
### \<Longrightarrow> integrable ?M (indicator ?A)
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ambiguous input (line 1939 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X)))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" X)
###           ("\<^const>Fun.comp" ("_position" f) ("_position" X)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X)))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###         ("\<^const>Fun.comp" ("_position" f) ("_position" X))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### inverse ?a1 \<equiv> (1::?'a1) / ?a1
### Ignoring duplicate rewrite rule:
### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1)
### Ignoring duplicate rewrite rule:
### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
### Ignoring duplicate rewrite rule:
### frontier {..?a1} \<equiv> {?a1}
### Ambiguous input (line 1868 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Z))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.entropy_Pow"
###         ("\<^const>HOL.disj" ("_position" X) ("_position" Z))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>local.mutual_information_Pow" ("_position" X)
###       ("_position" Z))
###     ("\<^const>Groups.minus_class.minus"
###       ("\<^const>local.entropy_Pow" ("_position" X))
###       ("\<^const>local.conditional_entropy_Pow" ("_position" X)
###         ("_position" Z)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.


More information about the isabelle-dev mailing list