diff -r 2c3e5e58d93f -r 154cf64e403e src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Feb 04 16:01:44 2019 +0100 +++ b/src/HOL/Library/Library.thy Mon Feb 04 15:39:37 2019 +0100 @@ -63,6 +63,7 @@ Perm Permutation Permutations + Power_By_Squaring Preorder Product_Plus Quadratic_Discriminant