equal
deleted
inserted
replaced
51 typedecl i |
51 typedecl i |
52 arities i :: "term" |
52 arities i :: "term" |
53 |
53 |
54 |
54 |
55 interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) |
55 interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) |
56 (* both X and Y get type 'b since 'b is the internal type of parameter b, |
|
57 not wanted, but put up with for now. *) |
|
58 |
56 |
59 print_interps A |
57 print_interps A |
60 |
58 |
61 (* possible accesses *) |
59 (* possible accesses *) |
62 thm p1.a.asm_A thm LocaleTest.p1.a.asm_A |
60 thm p1.a.asm_A thm LocaleTest.p1.a.asm_A |
63 thm LocaleTest.asm_A thm p1.asm_A |
61 thm p1.asm_A thm LocaleTest.p1.asm_A |
64 |
62 |
65 |
63 |
66 (* without prefix *) |
64 (* without prefix *) |
67 |
65 |
68 interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro) |
66 interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro) |