
diff -r 8f493d371234 -r 1476c26d4310 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 13:24:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 14:44:18 2010 +0200
@@ -797,13 +797,13 @@
 
   Isabelle provides a set of \emph{mono} rules, that are used to split implications
   of similar statements into simpler implication subgoals. These are enhanced
-  with special quotient theorem in the regularization goal. Below we only show
+  with special quotient theorem in the regularization proof. Below we only show
   the versions for the universal quantifier. For the existential quantifier
   and abstraction they are analogous.
 
   First, bounded universal quantifiers can be removed on the right:
 
-  @{thm [display, indent=10] ball_reg_right[no_vars]}
+  @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}
 
   They can be removed anywhere if the relation is an equivalence relation:
 




