--- a/QuotMain.thy	Fri Sep 25 17:08:50 2009 +0200
+++ b/QuotMain.thy	Fri Sep 25 19:26:18 2009 +0200
@@ -156,14 +156,6 @@
 end
 *}
 
-
-ML {*
-  typedef_term @{term "x::nat\<Rightarrow>nat\<Rightarrow>bool"} @{typ nat} @{context}
-  |> Syntax.string_of_term @{context} 
-  |> writeln
-*}
-
-
 ML {*
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
@@ -183,7 +175,7 @@
 *}
 
 ML {*
-(* proves the QUOT_TYPE theorem for the new type *)
+(* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
   val rep_thm = #Rep typedef_info
@@ -215,6 +207,7 @@
 *}
 
 ML {*
+(* proves the quotient theorem *)
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
   val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
@@ -711,8 +704,16 @@
 
 
 text {*
-  unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)'
-  to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left.
+  Unlam_def converts a definition given as 
+
+    c \<equiv> %x. %y. f x y
+
+  to a theorem of the form 
+   
+    c x y \<equiv> f x y 
+
+  This function is needed to rewrite the right-hand
+  side to the left-hand side.
 *}
 
 ML {*
@@ -853,6 +854,8 @@
   Logic.mk_equals ((build_aux concl2), concl2)
 end *}
 
+thm EMPTY_def IN_def UNION_def
+
 ML {* val emptyt = symmetric (unlam_def  @{context} @{thm EMPTY_def}) *}
 ML {* val in_t =   symmetric (unlam_def  @{context} @{thm IN_def}) *}
 ML {* val uniont = symmetric (unlam_def @{context}  @{thm UNION_def}) *}