--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 15:53:42 2018 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 19:28:05 2018 +0100
@@ -521,6 +521,15 @@
x.lor_triv
+subsection \<open>Rewrite morphisms in expressions\<close>
+
+interpretation y: logic_o "(\<or>)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
+proof -
+ show bool_logic_o: "PROP logic_o((\<or>), Not)" by unfold_locales fast+
+ show "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast
+qed
+
+
subsection \<open>Inheritance of rewrite morphisms\<close>
locale reflexive =