# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276519458 -7200
# Node ID 1476c26d431041e0669b6b17d38f71227eaa798f
# Parent  8f493d371234dc04d892ea73996af6ba3157f0ed
qpaper/unfold the ball_reg_right statement

diff -r 8f493d371234 -r 1476c26d4310 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Jun 14 13:24:22 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 14:44:18 2010 +0200
@@ -1662,5 +1662,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 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: