Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/ex/Locale_Test/Locale_Test3.thy
author wenzelm
Sun, 13 Aug 2023 19:27:58 +0200
changeset 78528 3d6dbf215559
parent 69590 e65314985426
permissions -rw-r--r--
clarified command arguments: optionally restrict to given theories (from theory loader);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37134
29bd6c2ffba8 Revise locale test theory layout.
ballarin
parents:
diff changeset 
     1
 
(*  Title:      FOL/ex/Locale_Test/Locale_Test3.thy
29bd6c2ffba8 Revise locale test theory layout.
ballarin
parents:
diff changeset 
     2
 
    Author:     Clemens Ballarin
29bd6c2ffba8 Revise locale test theory layout.
ballarin
parents:
diff changeset 
     3
 












29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     4


Test environment for the locale implementation.













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     5


*)













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     6














29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     7


theory Locale_Test3













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     8


imports Locale_Test1













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




     9


begin













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    10









69590






e65314985426
isabelle update_inner_syntax_cartouches;



wenzelm


parents: 
61566

diff
changeset




    11


interpretation le2: mixin_thy_merge \<open>gle\<close> \<open>gle'\<close>













e65314985426
isabelle update_inner_syntax_cartouches;



wenzelm


parents: 
61566

diff
changeset




    12


  rewrites \<open>reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)\<close>








37134






29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    13


proof -








69590






e65314985426
isabelle update_inner_syntax_cartouches;



wenzelm


parents: 
61566

diff
changeset




    14


  show \<open>mixin_thy_merge(gle, gle')\<close> by unfold_locales








37134






29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    15


  note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]








69590






e65314985426
isabelle update_inner_syntax_cartouches;



wenzelm


parents: 
61566

diff
changeset




    16


  show \<open>reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)\<close>








37134






29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    17


    by (simp add: reflexive.less_def[OF reflexive] gless'_def)













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    18


qed













29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    19














29bd6c2ffba8
Revise locale test theory layout.



ballarin


parents: 

diff
changeset




    20


end















isabelle