changeset 59897 | d1e7f56bcd79 |
parent 56138 | f42de6d8ed8e |
child 60770 | 240563fbf41d |
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Apr 01 18:17:44 2015 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Apr 01 18:18:12 2015 +0200 @@ -775,7 +775,7 @@ locale container begin -interpretation private!: roundup True by unfold_locales rule +interpretation "private"!: roundup True by unfold_locales rule lemmas true_copy = private.true end