--- a/Quotient-Paper/Paper.thy	Sat Jun 05 08:02:39 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 05 10:03:42 2010 +0200
@@ -521,7 +521,49 @@
 
 section {* Examples *}
 
+(* Mention why equivalence *)
 
+text {*
+
+  A user of our quotient package first needs to define an equivalence relation:
+
+  @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}
+
+  Then the user defines a quotient type:
+
+  @{text "quotient_type int = (nat \<times> nat) / \<approx>"}
+
+  Which leaves a proof obligation that the relation is an equivalence relation,
+  that can be solved with the automatic tactic with two definitions.
+
+  The user can then specify the constants on the quotient type:
+
+  @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
+  @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
+  @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}
+
+  Lets first take a simple theorem about addition on the raw level:
+
+  @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}
+
+  When the user tries to lift a theorem about integer addition, the respectfulness
+  proof obligation is left, so let us prove it first:
+  
+  @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
+
+  Can be proved automatically by the system just by unfolding the definition
+  of @{term "op \<Longrightarrow>"}.
+
+  Now the user can either prove a lifted lemma explicitely:
+
+  @{text "lemma 0 + i = i by lifting plus_zero_raw"}
+
+  Or in this simple case use the automated translation mechanism:
+
+  @{text "thm plus_zero_raw[quot_lifted]"}
+
+  obtaining the same result.
+*}
 
 section {* Related Work *}
 
@@ -549,6 +591,8 @@
   \end{itemize}
 *}
 
+section {* Conclusion *}
+
 (*<*)
 end
 (*>*)