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/Nominal/Examples/Class2.thy
changeset 80914 d97fdabd9e2b
parent 80609 4b5d3d0abb69
child 81543 fa37ee54644c 
--- a/src/HOL/Nominal/Examples/Class2.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -2949,12 +2949,12 @@
 done
 
 abbreviation
-  CANDn::"ty \<Rightarrow> ntrm set"  ("\<parallel>'(_')\<parallel>" [60] 60) 
+  CANDn::"ty \<Rightarrow> ntrm set"  (\<open>\<parallel>'(_')\<parallel>\<close> [60] 60) 
 where
   "\<parallel>(B)\<parallel> \<equiv> lfp (NEGn B \<circ> NEGc B)" 
 
 abbreviation
-  CANDc::"ty \<Rightarrow> ctrm set"  ("\<parallel><_>\<parallel>" [60] 60)
+  CANDc::"ty \<Rightarrow> ctrm set"  (\<open>\<parallel><_>\<parallel>\<close> [60] 60)
 where
   "\<parallel><B>\<parallel> \<equiv> NEGc B (\<parallel>(B)\<parallel>)"
isabelle