changeset 71393 | fce780f9c9c6 |
parent 71036 | dfcc1882d05a |
child 71956 | a4bffc0de967 |
--- a/src/HOL/Library/Library.thy Fri Jan 17 18:58:58 2020 +0100 +++ b/src/HOL/Library/Library.thy Sun Jan 19 07:50:35 2020 +0100 @@ -14,6 +14,8 @@ Combine_PER Complete_Partial_Order2 Conditional_Parametricity + Confluence + Confluent_Quotient Countable Countable_Complete_Lattices Countable_Set_Type