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/Comp/Priority.thy
changeset 69597 ff784d5a5bfb
parent 67613 ce654b0e6d69 
--- a/src/HOL/UNITY/Comp/Priority.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -254,8 +254,8 @@
 
 
 text\<open>We have proved all (relevant) theorems given in the paper.  We didn't
-assume any thing about the relation @{term r}.  It is not necessary that
-@{term r} be a priority relation as assumed in the original proof.  It
+assume any thing about the relation \<^term>\<open>r\<close>.  It is not necessary that
+\<^term>\<open>r\<close> be a priority relation as assumed in the original proof.  It
 suffices that we start from a state which is finite and acyclic.\<close>
isabelle