src/HOL/HOL.thy
changeset 15392 290bc97038c7
parent 15380 455cfa766dad
child 15411 1d195de59497