src/FOL/ex/LocaleTest.thy

--- a/src/FOL/ex/LocaleTest.thy	Sun May 23 19:30:29 2010 -0700
+++ b/src/FOL/ex/LocaleTest.thy	Mon May 24 10:48:32 2010 +0200
@@ -533,7 +533,7 @@
   grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
   grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
 
-text {* Mixin not applied to locales further up the hierachy. *}
+text {* Setup *}
 
 locale mixin = reflexive
 begin
@@ -548,16 +548,6 @@
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
-thm le.less_def  (* mixin not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
-thm le.less_thm  (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
-
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
-  by (rule le.less_def)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
-  by (rule le.less_thm)
-
 text {* Mixin propagated along the locale hierarchy *}
 
 locale mixin2 = mixin