# HG changeset patch
# User ballarin
# Date 1378239167 -7200
# Node ID c8c548d83862d5b0cbf3963067de1ea6ab3edc9b
# Parent  643e1151ed7ecd31f161031b9c81535f315ea25a
Terminology: mixin -> rewrite morphism.

diff -r 643e1151ed7e -r c8c548d83862 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 02 17:57:56 2013 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Sep 03 22:12:47 2013 +0200
@@ -484,7 +484,9 @@
   by unfold_locales
 
 
-subsection {* Equations *}
+subsection {* Interpretation *}
+
+subsection {* Rewrite morphism *}
 
 locale logic_o =
   fixes land (infixl "&&" 55)
@@ -516,7 +518,7 @@
   x.lor_triv
 
 
-subsection {* Inheritance of mixins *}
+subsection {* Inheritance of rewrite morphisms *}
 
 locale reflexive =
   fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
@@ -549,7 +551,7 @@
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
-text {* Mixin propagated along the locale hierarchy *}
+text {* Rewrite morphism propagated along the locale hierarchy *}
 
 locale mixin2 = mixin
 begin
@@ -559,11 +561,11 @@
 interpretation le: mixin2 gle
   by unfold_locales
 
-thm le.less_thm2  (* mixin applied *)
+thm le.less_thm2  (* rewrite morphism applied *)
 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   by (rule le.less_thm2)
 
-text {* Mixin does not leak to a side branch. *}
+text {* Rewrite morphism does not leak to a side branch. *}
 
 locale mixin3 = reflexive
 begin
@@ -573,10 +575,10 @@
 interpretation le: mixin3 gle
   by unfold_locales
 
-thm le.less_thm3  (* mixin not applied *)
+thm le.less_thm3  (* rewrite morphism not applied *)
 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
 
-text {* Mixin only available in original context *}
+text {* Rewrite morphism only available in original context *}
 
 locale mixin4_base = reflexive
 
@@ -604,11 +606,11 @@
 interpretation le4: mixin4_combined gle' gle
   by unfold_locales (rule grefl')
 
-thm le4.less_thm4' (* mixin not applied *)
+thm le4.less_thm4' (* rewrite morphism not applied *)
 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   by (rule le4.less_thm4')
 
-text {* Inherited mixin applied to new theorem *}
+text {* Inherited rewrite morphism applied to new theorem *}
 
 locale mixin5_base = reflexive
 
@@ -628,11 +630,11 @@
 
 lemmas (in mixin5_inherited) less_thm5 = less_def
 
-thm le5.less_thm5  (* mixin applied *)
+thm le5.less_thm5  (* rewrite morphism applied *)
 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   by (rule le5.less_thm5)
 
-text {* Mixin pushed down to existing inherited locale *}
+text {* Rewrite morphism pushed down to existing inherited locale *}
 
 locale mixin6_base = reflexive
 
@@ -657,7 +659,7 @@
 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   by (rule le6.less_thm6)
 
-text {* Existing mixin inherited through sublocale relation *}
+text {* Existing rewrite morphism inherited through sublocale relation *}
 
 locale mixin7_base = reflexive
 
@@ -677,7 +679,7 @@
 
 lemmas (in mixin7_inherited) less_thm7 = less_def
 
-thm le7.less_thm7  (* before, mixin not applied *)
+thm le7.less_thm7  (* before, rewrite morphism not applied *)
 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   by (rule le7.less_thm7)
 
@@ -696,7 +698,7 @@
 locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
 
 
-subsection {* Mixins in sublocale *}
+subsection {* Rewrite morphisms in sublocale *}
 
 text {* Simulate a specification of left groups where unit and inverse are defined
   rather than specified.  This is possible, but not in FOL, due to the lack of a
@@ -745,7 +747,7 @@
 lemma "dgrp.one(prod) = one" by (rule one_equation)
 lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
 
-text {* Mixins applied *}
+text {* Rewrite morphisms applied *}
 
 lemma "one = glob_one(prod)" by (rule one_def)
 lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
@@ -757,7 +759,7 @@
 lemma "0 = glob_one (op +)" by (rule int.def.one_def)
 lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
 
-text {* Roundup applies mixins at declaration level in DFS tree *}
+text {* Roundup applies rewrite morphisms at declaration level in DFS tree *}
 
 locale roundup = fixes x assumes true: "x <-> True"