diff -r ce774af6b964 -r a792bfc1be2b Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:38:42 2010 +0100
@@ -382,10 +382,6 @@
 
 lemma  "All (\<lambda>(x::'a fset, y). x = y)"
 apply(lifting test)
-apply(cleaning)
-thm all_prs
-apply(rule all_prs)
-apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
 done
 
 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"
@@ -393,14 +389,6 @@
 
 lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"
 apply(lifting test2)
-apply(cleaning)
-apply(rule ex_prs)
-apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
 done
 
-ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *}
-
-
-
-
 end