# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276581513 -7200
# Node ID 9c44db3eef95cf5143f3df94370e882b0854fb1b
# Parent  2a95188263ec955321c4710840f74dc9f413f18b
Remove only reference to 'equivp'.

diff -r 2a95188263ec -r 9c44db3eef95 Quotient-Paper/Paper.thy
--- 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: