equal
deleted
inserted
replaced
90 * The old proof method "default" has been removed (legacy since |
90 * The old proof method "default" has been removed (legacy since |
91 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
91 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
92 |
92 |
93 |
93 |
94 *** HOL *** |
94 *** HOL *** |
|
95 |
|
96 * Probability/Random_Permutations.thy contains some theory about |
|
97 choosing a permutation of a set uniformly at random and folding over a |
|
98 list in random order. |
|
99 |
|
100 * Library/Set_Permutations.thy (executably) defines the set of |
|
101 permutations of a set, i.e. the set of all lists that contain every |
|
102 element of the carrier set exactly once. |
95 |
103 |
96 * New abbreviations for negated existence (but not bounded existence): |
104 * New abbreviations for negated existence (but not bounded existence): |
97 |
105 |
98 \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
106 \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
99 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
107 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |