diff -r e417be53916e -r 200954544cae Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon May 10 18:09:00 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue May 11 12:18:26 2010 +0100
@@ -11,7 +11,27 @@
 
 section {* Introduction *}
 
-text {* TBD *}
+text {* 
+  Isabelle is a generic theorem prover in which many logics can be implemented. 
+  The most widely used one, however, is
+  Higher-Order Logic (HOL). This logic 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 
+  mechanisms for extending the logic: one is the definition of new constants
+  in terms of existing ones; the other is the introduction of new types
+  by identifying non-empty subsets in existing types. It is well understood 
+  to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
+  For example the integers in Isabelle/HOL are constructed by a quotient construction over 
+  the type @{typ "nat \<times> nat"} and the equivalence relation
+
+  @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
+
+  \noindent
+  The problem is that one 
+  
+
+
+*}
 
 subsection {* Contributions *}