--- a/FSet.thy Tue Dec 01 19:01:51 2009 +0100
+++ b/FSet.thy Tue Dec 01 19:18:43 2009 +0100
@@ -304,7 +304,6 @@
thm m1
-
lemma "IN x EMPTY = False"
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})