Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/PPROD.thy
changeset 69597 ff784d5a5bfb
parent 67613 ce654b0e6d69 
--- a/src/HOL/UNITY/PPROD.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -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\<open>This holds because the @{term "F j"} cannot change @{term "lift_set i"}\<close>
+text\<open>This holds because the \<^term>\<open>F j\<close> cannot change \<^term>\<open>lift_set i\<close>\<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,7 +114,7 @@
 
 (*** guarantees properties ***)
 
-text\<open>This rule looks unsatisfactory because it refers to @{term lift}. 
+text\<open>This rule looks unsatisfactory because it refers to \<^term>\<open>lift\<close>. 
   One must use
   \<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
isabelle