changeset 65099 | 30d0b2f1df76 |
parent 65050 | 4538153bcc5c |
child 65374 | a5b38d8d3c1e |
--- a/src/HOL/ROOT Fri Mar 03 23:21:24 2017 +0100 +++ b/src/HOL/ROOT Thu Mar 02 21:16:02 2017 +0100 @@ -297,7 +297,9 @@ "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Library/Permutation" theories - (*** New development, based on explicit structures ***) + (* Orders and Lattices *) + Galois_Connection (* Knaster-Tarski theorem and Galois connections *) + (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *)