src/HOL/Library/Product_Lattice.thy
changeset 44798 9900c0069ae6
parent 44006 b9839fad3bb6
child 44928 7ef6505bde7f