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