--- a/FSet.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/FSet.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -14,9 +14,7 @@
 
 lemma list_eq_refl:
   shows "xs \<approx> xs"
-  apply (induct xs)
-   apply (auto intro: list_eq.intros)
-  done
+  by (induct xs) (auto intro: list_eq.intros)
 
 lemma equiv_list_eq:
   shows "EQUIV list_eq"
@@ -178,7 +176,7 @@
 
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
-lemma memb_rsp[quot_rsp]:
+lemma memb_rsp:
   fixes z
   assumes a: "x \<approx> y"
   shows "(z memb x) = (z memb y)"
@@ -188,7 +186,7 @@
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
-lemma card1_rsp[quot_rsp]:
+lemma card1_rsp:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
@@ -246,7 +244,7 @@
   apply (rule rev_rsp)
   done
 
-lemma append_rsp[quot_rsp]:
+lemma append_rsp:
   assumes a : "l1 \<approx> r1"
   assumes b : "l2 \<approx> r2 "
   shows "(l1 @ l2) \<approx> (r1 @ r2)"
@@ -265,7 +263,7 @@
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
-lemma map_rsp[quot_rsp]:
+lemma map_rsp:
   assumes a: "a \<approx> b"
   shows "map f a \<approx> map f b"
   using a