--- a/src/FOL/ex/NewLocaleTest.thy Fri Dec 12 19:58:26 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Sun Dec 14 15:43:04 2008 +0100
@@ -421,7 +421,7 @@
end
-interpretation x: logic_o "op &" "Not"
+interpretation x!: logic_o "op &" "Not"
where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
proof -
show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
@@ -431,9 +431,12 @@
thm x.lor_o_def bool_logic_o
+lemma lor_triv: "z <-> z" ..
+
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
-thm x.lor_triv
+thm lor_triv [where z = True] (* Check strict prefix. *)
+ x.lor_triv
subsection {* Interpretation in proofs *}