Changes

Summary

Added proof method for Pratt Certificates
Merged
Updated Randomised_Social_Choice/SDS_Impossibility to work with ennreal

Changeset 6610:f922f246c322 by manuel eberl _eberlm@in.tum.de_: Added proof method for Pratt Certificates
The file was added	`thys/Pratt_Certificate/pratt.ML`
The file was modified	`thys/Pratt_Certificate/Pratt_Certificate.thy` (diff)
Changeset 6609:e8008380c946 by manuel eberl _eberlm@in.tum.de_: Merged
Changeset 6608:e6f5f61291b8 by manuel eberl _eberlm@in.tum.de_: Updated Randomised_Social_Choice/SDS_Impossibility to work with ennreal
The file was modified	`thys/Pratt_Certificate/Pratt_Certificate.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Automation/sds_automation.ML` (diff)
The file was modified	`thys/Randomised_Social_Choice/Missing_PMF.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Order_Predicates.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/PMF_Of_List.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Preference_Profiles.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Random_Dictatorship.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Random_Permutations.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Random_Serial_Dictatorship.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/SD_Efficiency.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Set_Permutations.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Social_Decision_Schemes.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Stochastic_Dominance.thy` (diff)
The file was modified	`thys/SDS_Impossibility/SDS_Impossibility.thy` (diff)