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/Example.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/NanoJava/Example.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/NanoJava/Example.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -49,13 +49,13 @@
 subsection "Program representation"
 
 axiomatization 
-  N    :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
+  N    :: cname (\<open>Nat\<close>) (* with mixfix because of clash with NatDef.Nat *)
   and pred :: fname
   and suc add :: mname
   and any  :: vname
 
 abbreviation
-  dummy :: expr ("<>")
+  dummy :: expr (\<open><>\<close>)
   where "<> == LAcc any"
 
 abbreviation
@@ -92,7 +92,7 @@
 
 subsection "``atleast'' relation for interpretation of Nat ``values''"
 
-primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
+primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" (\<open>_:_ \<ge> _\<close> [51, 51, 51] 50) where
   "s:x\<ge>0     = (x\<noteq>Null)"
 | "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
isabelle