Changes

Summary

Probability: move emeasure and nn_integral from ereal to ennreal

Changeset 6511:9a171adc5015 by hoelzl: Probability: move emeasure and nn_integral from ereal to ennreal
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/Density_Compiler/Density_Predicates.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Compiler.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Compiler_Pred.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Density_Contexts.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Target_Density_Contexts.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Target_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Transformations.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Values.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Conditional_Expectation.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Ergodicity.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Invariants.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Kingman.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Measure_Preserving_Transformations.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Recurrence.thy` (diff)
The file was modified	`thys/Ergodic_Theory/SG_Library_Complement.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Markov_Models/Discrete_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/MDP_Reachability_Problem.thy` (diff)
The file was modified	`thys/Markov_Models/Markov_Decision_Process.thy` (diff)
The file was modified	`thys/Markov_Models/Trace_Space_Equals_Markov_Processes.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Example_A.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Example_B.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Markov_Models/ex/MDP_RP_Certification.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PCTL.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PGCL.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Zeroconf_Analysis.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Concrete.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Trace_Based.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy` (diff)
The file was removed	`thys/Ergodic_Theory/document/root.tex`