| changeset 80914 | d97fdabd9e2b |
| parent 67613 | ce654b0e6d69 |
| child 81292 | 137b0b107c4b |
--- a/src/HOL/Proofs/Lambda/ParRed.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/Proofs/Lambda/ParRed.thy Fri Sep 20 19:51:08 2024 +0200 @@ -13,7 +13,7 @@ subsection \<open>Parallel reduction\<close> -inductive par_beta :: "[dB, dB] => bool" (infixl "=>" 50) +inductive par_beta :: "[dB, dB] => bool" (infixl \<open>=>\<close> 50) where var [simp, intro!]: "Var n => Var n" | abs [simp, intro!]: "s => t ==> Abs s => Abs t"