| changeset 69597 | ff784d5a5bfb |
| parent 67399 | eab6ce8368fa |
| child 71989 | bad75618fb82 |
--- a/src/HOL/Nominal/Examples/Standardization.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Nominal/Examples/Standardization.thy Sat Jan 05 17:24:33 2019 +0100 @@ -682,7 +682,7 @@ qed text \<open> -@{term NF} characterizes exactly the terms that are in normal form. +\<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form. \<close> lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"