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/NanoJava/TypeRel.thy
changeset 80914 d97fdabd9e2b
parent 68451 c34aa23a1fb6 
--- a/src/HOL/NanoJava/TypeRel.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -15,10 +15,10 @@
   "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
 
 abbreviation
-  subcls1_syntax :: "[cname, cname] => bool"  ("_ \<prec>C1 _" [71,71] 70)
+  subcls1_syntax :: "[cname, cname] => bool"  (\<open>_ \<prec>C1 _\<close> [71,71] 70)
   where "C \<prec>C1 D == (C,D) \<in> subcls1"
 abbreviation
-  subcls_syntax  :: "[cname, cname] => bool" ("_ \<preceq>C _"  [71,71] 70)
+  subcls_syntax  :: "[cname, cname] => bool" (\<open>_ \<preceq>C _\<close>  [71,71] 70)
   where "C \<preceq>C D \<equiv> (C,D) \<in> subcls1\<^sup>*"
 
 
@@ -26,7 +26,7 @@
 
 text\<open>Widening, viz. method invocation conversion\<close>
 inductive
-  widen :: "ty => ty => bool"  ("_ \<preceq> _" [71,71] 70)
+  widen :: "ty => ty => bool"  (\<open>_ \<preceq> _\<close> [71,71] 70)
 where
   refl [intro!, simp]: "T \<preceq> T"
 | subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
isabelle