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