src/HOL/ex/LocaleTest2.thy
changeset 27885 76b51cd0a37c
parent 27556 292098f2efdf
child 28823 dcbef866c9e2