# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276519540 -7200
# Node ID c3fd4e42bb4a7e51441632c36bf45ad31f3ed4db
# Parent  1476c26d431041e0669b6b17d38f71227eaa798f# Parent  a040404748006a95da56446ce5e8b1a3f68b2be2
merge

diff -r a04040474800 -r c3fd4e42bb4a Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Jun 14 12:30:08 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 14:45:40 2010 +0200
@@ -1672,5 +1672,10 @@
 apply(auto simp add: mem_def)
 done
 
+lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
+apply rule
+apply (rule ball_reg_right)
+apply auto
+done
 
 end
diff -r a04040474800 -r c3fd4e42bb4a Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 12:30:08 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 14:45:40 2010 +0200
@@ -816,13 +816,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: