src/HOL/ex/LocaleTest2.thy
changeset 25897 e9d45709bece
parent 25592 e8ddaf6bf5df
child 27556 292098f2efdf