diff -r 0d34f2e60d5d -r aeb4fc74984f QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 11:17:27 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:20:50 2009 +0200
@@ -329,14 +329,9 @@
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
-(* Babs p m = \<lambda>x. if x \<in> p then m x else undefined *)
-
-(*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where
-  "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
-
-
-ML {* exists *}
-ML {* mem *}
+(* TODO: Consider defining it with an "if"; sth like:
+   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
 
 ML {*
 fun needs_lift (rty as Type (rty_s, _)) ty =