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/Proofs/Lambda/Eta.thy
changeset 80914 d97fdabd9e2b
parent 76987 4c275405faae 
--- a/src/HOL/Proofs/Lambda/Eta.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -18,7 +18,7 @@
   | "free (Abs s) i = free s (i + 1)"
 
 inductive
-  eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
+  eta :: "[dB, dB] => bool"  (infixl \<open>\<rightarrow>\<^sub>\<eta>\<close> 50)
 where
     eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]"
   | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u"
@@ -26,11 +26,11 @@
   | abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t"
 
 abbreviation
-  eta_reds :: "[dB, dB] => bool"   (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) where
+  eta_reds :: "[dB, dB] => bool"   (infixl \<open>\<rightarrow>\<^sub>\<eta>\<^sup>*\<close> 50) where
   "s \<rightarrow>\<^sub>\<eta>\<^sup>* t == eta\<^sup>*\<^sup>* s t"
 
 abbreviation
-  eta_red0 :: "[dB, dB] => bool"   (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50) where
+  eta_red0 :: "[dB, dB] => bool"   (infixl \<open>\<rightarrow>\<^sub>\<eta>\<^sup>=\<close> 50) where
   "s \<rightarrow>\<^sub>\<eta>\<^sup>= t == eta\<^sup>=\<^sup>= s t"
 
 inductive_cases eta_cases [elim!]:
isabelle