Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quotient-Paper/Paper.thy
changeset 2265 9c44db3eef95
parent 2264 2a95188263ec
child 2266 dcffc2f132c9
child 2269 e4699a240d2c 
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 07:54:30 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 07:58:33 2010 +0200
@@ -874,7 +874,7 @@
 
   They can be removed anywhere if the relation is an equivalence relation:
 
-  @{thm [display, indent=10] ball_reg_eqv[no_vars]}
+  @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
 
   And finally it can be removed anywhere if @{term R2} is an equivalence relation:
nominal2