Mercurial Mercurial > repos > isabelle / diff
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_Test.thy
changeset 69590 e65314985426
parent 61489 b8d375aee0df 
--- a/src/FOL/ex/Locale_Test/Locale_Test.thy	Thu Jan 03 21:48:05 2019 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test.thy	Thu Jan 03 22:19:19 2019 +0100
@@ -16,9 +16,9 @@
 lemmas less_mixin_thy_merge2 = le'.less_def
 end
 
-lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" (* mixin from first interpretation applied *)
+lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close> (* mixin from first interpretation applied *)
   by (rule le1.less_mixin_thy_merge1)
-lemma "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y" (* mixin from second interpretation applied *)
+lemma \<open>gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y\<close> (* mixin from second interpretation applied *)
   by (rule le1.less_mixin_thy_merge2)
 
 end
isabelle