--- a/src/HOL/UNITY/PPROD.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/PPROD.thy Wed May 25 11:50:58 2016 +0200
@@ -68,7 +68,7 @@
PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
by (simp add: JN_transient PLam_def)
-text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
+text\<open>This holds because the @{term "F j"} cannot change @{term "lift_set i"}\<close>
lemma PLam_ensures:
"[| i \<in> I; F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
\<forall>j. F j \<in> preserves snd |]
@@ -114,11 +114,11 @@
(*** guarantees properties ***)
-text{*This rule looks unsatisfactory because it refers to @{term lift}.
+text\<open>This rule looks unsatisfactory because it refers to @{term lift}.
One must use
- @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
- something like @{text lift_preserves_sub} to rewrite the third. However
- there's no obvious alternative for the third premise.*}
+ \<open>lift_guarantees_eq_lift_inv\<close> to rewrite the first subgoal and
+ something like \<open>lift_preserves_sub\<close> to rewrite the third. However
+ there's no obvious alternative for the third premise.\<close>
lemma guarantees_PLam_I:
"[| lift i (F i): X guarantees Y; i \<in> I;
OK I (%i. lift i (F i)) |]