equal
deleted
inserted
replaced
14 begin |
14 begin |
15 lemmas less_mixin_thy_merge1 = le.less_def |
15 lemmas less_mixin_thy_merge1 = le.less_def |
16 lemmas less_mixin_thy_merge2 = le'.less_def |
16 lemmas less_mixin_thy_merge2 = le'.less_def |
17 end |
17 end |
18 |
18 |
19 lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" (* mixin from first interpretation applied *) |
19 lemma \<open>gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y\<close> (* mixin from first interpretation applied *) |
20 by (rule le1.less_mixin_thy_merge1) |
20 by (rule le1.less_mixin_thy_merge1) |
21 lemma "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y" (* mixin from second interpretation applied *) |
21 lemma \<open>gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y\<close> (* mixin from second interpretation applied *) |
22 by (rule le1.less_mixin_thy_merge2) |
22 by (rule le1.less_mixin_thy_merge2) |
23 |
23 |
24 end |
24 end |