src/HOL/ex/LocaleTest2.thy
changeset 28603 b40800eef8a7
parent 27556 292098f2efdf
child 28823 dcbef866c9e2