| changeset 25972 | 94b15338da8d |
| parent 23750 | a1db5f819d00 |
| child 35440 | bdf8ad377877 |
--- a/src/HOL/Lambda/ParRed.thy Fri Jan 25 22:04:46 2008 +0100 +++ b/src/HOL/Lambda/ParRed.thy Fri Jan 25 23:05:23 2008 +0100 @@ -55,7 +55,7 @@ done -subsection {* Misc properties of par-beta *} +subsection {* Misc properties of @{text "par_beta"} *} lemma par_beta_lift [simp]: "t => t' \<Longrightarrow> lift t n => lift t' n"