| changeset 62390 | 842917225d56 |
| parent 62374 | cb27a55d868a |
| child 69260 | 0a9688695a1b |
--- a/src/HOL/Library/Countable_Complete_Lattices.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy Tue Feb 23 16:25:08 2016 +0100 @@ -274,4 +274,4 @@ subclass (in complete_distrib_lattice) countable_complete_distrib_lattice by standard (auto intro: sup_Inf inf_Sup) -end \ No newline at end of file +end