src/HOL/ex/Locales.thy
changeset 13256 cf85c4f7dcf2
parent 13107 8743cc847224
child 13383 041d78bf9403