|
37134
|
1 |
(* Title: FOL/ex/Locale_Test/Locale_Test3.thy
|
|
|
2 |
Author: Clemens Ballarin
|
|
|
3 |
|
|
|
4 |
Test environment for the locale implementation.
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
theory Locale_Test3
|
|
|
8 |
imports Locale_Test1
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
interpretation le2: mixin_thy_merge gle gle'
|
|
61489
|
12 |
where "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
|
|
37134
|
13 |
proof -
|
|
|
14 |
show "mixin_thy_merge(gle, gle')" by unfold_locales
|
|
|
15 |
note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
|
|
61489
|
16 |
show "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
|
|
37134
|
17 |
by (simp add: reflexive.less_def[OF reflexive] gless'_def)
|
|
|
18 |
qed
|
|
|
19 |
|
|
|
20 |
end
|