| changeset 69593 | 3dda49e08b9d |
| parent 68490 | eb53f944c8cd |
| child 76213 | e44d86131648 |
--- a/src/ZF/Epsilon.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/ZF/Epsilon.thy Fri Jan 04 23:22:53 2019 +0100 @@ -80,7 +80,7 @@ by (rule arg_in_eclose_sing [THEN eclose_induct], blast) -subsection\<open>Leastness of @{term eclose}\<close> +subsection\<open>Leastness of \<^term>\<open>eclose\<close>\<close> (** eclose(A) is the least transitive set including A as a subset. **)