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/Height.thy
changeset 80914 d97fdabd9e2b
parent 66453 cc19f7ca2ed6 
--- a/src/HOL/Nominal/Examples/Height.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,7 +12,7 @@
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
-  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+  | Lam "\<guillemotleft>name\<guillemotright>lam" (\<open>Lam [_]._\<close> [100,100] 100)
 
 text \<open>Definition of the height-function on lambda-terms.\<close> 
 
@@ -31,7 +31,7 @@
 text \<open>Definition of capture-avoiding substitution.\<close>
 
 nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  (\<open>_[_::=_]\<close> [100,100,100] 100)
 where
   "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
 | "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
isabelle