Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed comment;
authorwenzelm
Wed, 03 Jul 2002 14:52:57 +0200
changeset 13288 9a870391ff66
parent 13287 e4134f9eb4dc
child 13289 53e201efdaa2
fixed comment;
src/ZF/Univ.thy file | annotate | diff | comparison | revisions 
--- a/src/ZF/Univ.thy	Wed Jul 03 10:02:15 2002 +0200
+++ b/src/ZF/Univ.thy	Wed Jul 03 14:52:57 2002 +0200
@@ -70,7 +70,7 @@
 apply (subst Vfrom)
 apply (rule subset_refl [THEN Un_mono])
 apply (rule UN_least)
-txt{*expand rank(x1) = (\<Union>y\<in>x1. succ(rank(y))) in assumptions*}
+txt{*expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions*}
 apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
 apply (rule subset_trans)
 apply (erule_tac [2] UN_upper)
isabelle