diff -r 9cb8f9a59402 -r b054cf6bd179 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 16:06:54 2009 +0200
+++ b/QuotMain.thy	Sun Oct 18 00:52:10 2009 +0200
@@ -3,6 +3,7 @@
 uses ("quotient.ML")
 begin
 
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -141,6 +142,7 @@
 
 end
 
+
 section {* type definition for the quotient type *}
 
 use "quotient.ML"
@@ -250,7 +252,6 @@
 
 ML {* lookup @{theory} @{type_name list} *}
 
-
 ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;