--- a/Nominal/Nominal2_Base.thy	Fri Jun 03 18:32:22 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Fri Jun 03 18:33:11 2011 +0900
@@ -1709,20 +1709,6 @@
   apply(rule THE_defaultI'[OF unique])
   done
 
-lemma fundef_ex1_eqvt2:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt_at G x"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
-  apply(simp only: f_def)
-  apply(subst the_default_eqvt)
-  apply(rule ex1)
-  using eqvt
-  unfolding eqvt_at_def
-  apply(simp)
-  done
-
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
@@ -1737,16 +1723,6 @@
   apply(simp add: permute_fun_app_eq)
   done
 
-lemma fundef_ex1_eqvt_at2:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt_at G x"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "eqvt_at f x"
-  unfolding eqvt_at_def
-  using assms
-  by (auto intro: fundef_ex1_eqvt2)
-
 lemma fundef_ex1_eqvt_at:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"

--- a/Quotient-Paper/Paper.thy	Fri Jun 03 18:32:22 2011 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Jun 03 18:33:11 2011 +0900
@@ -106,7 +106,7 @@
   theorem provers many questions concerning them are far from settled. In
   this paper we address the question of how to establish a convenient reasoning 
   infrastructure
-  for quotient constructions in the Isabelle/HOL, 
+  for quotient constructions in the Isabelle/HOL 
   theorem prover. Higher-Order Logic (HOL) consists
   of a small number of axioms and inference rules over a simply-typed
   term-language. Safe reasoning in HOL is ensured by two very restricted
@@ -531,7 +531,7 @@
   equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
   "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
   \eqref{listequiv}, respectively (the proofs about being equivalence
-  relations is omitted).  Given this data, we define for declarations shown in
+  relations are omitted).  Given this data, we define for declarations shown in
   \eqref{typedecl} the quotient types internally as
   
   \begin{isabelle}\ \ \ \ \ %%%