1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Locale_Abbrev_Test 8 imports Lib.Locale_Abbrev 9begin 10 11section \<open>Examples for @{command locale_abbrev}/@{command revert_abbrev}\<close> 12 13locale blah = 14 assumes X 15 fixes y 16begin 17 18definition "foo \<equiv> True" 19 20locale_abbrev "test \<equiv> foo" 21abbreviation "test2 \<equiv> y" 22abbreviation "test3 \<equiv> False" 23revert_abbrev test3 24abbreviation "test4 \<equiv> True" 25 26term test (* shows test, contracted, no fixed variable *) 27term test2 (* shows test2, contracted, fixed variable, not exportable *) 28term test3 (* shows test3, contracted, no fixed variable *) 29term test4 (* shows True, not contracted, no fixed variable *) 30 31end 32 33term test (* free variable, proper name is qualified *) 34term blah.test (* shows "blah.test", contracted *) 35term "blah.test2 y" (* shows "y", not contracted, needs fixed variable as parameter *) 36term blah.test3 (* shows "blah.test3", contracted *) 37term blah.test4 (* shows "True", not contracted *) 38 39 40locale blah2 = blah + 41 assumes Z 42begin 43 44(* unchanged from above on re-entering the context *) 45 46term test (* shows test, contracted, no fixed variable *) 47term test2 (* shows test2, contracted, fixed variable, not exportable *) 48term test3 (* shows test3, contracted, no fixed variable *) 49term test4 (* shows True, not contracted, no fixed variable *) 50 51end 52 53(* Can be used outside locales, but there is not really any point, because the 54 abbreviation command already provides everything *) 55locale_abbrev "test6 \<equiv> False" 56abbreviation "test5 \<equiv> False" 57 58(* revert_abbrev does not change anything outside locales, since the reverse abbreviation 59 is already present *) 60revert_abbrev test5 61revert_abbrev test6 62 63end