src/HOL/Library/Library.thy
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