--- a/Nominal/Abs.thy	Wed Apr 21 21:31:07 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 21:52:30 2010 +0200
@@ -129,16 +129,22 @@
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition
+  Abs ("[_]set. _" [60, 60] 60)
+where
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_res ("[_]res. _" [60, 60] 60)
+where
   "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_lst ("[_]lst. _" [60, 60] 60)
+where
   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 is
   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
@@ -169,9 +175,8 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  apply(simp_all add: alphas_abs)
-  apply(lifting alphas_abs)
-  done
+  unfolding alphas_abs
+  by (lifting alphas_abs)
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -327,9 +332,8 @@
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
-  apply(rule_tac [!] fresh_fun_eqvt_app)
-  apply(simp_all add: eqvts_raw)
-  done
+  by (rule_tac [!] fresh_fun_eqvt_app)
+     (simp_all add: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
@@ -337,36 +341,32 @@
   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
   unfolding supp_conv_fresh
-  apply(auto dest!: aux_fresh)
-  apply(simp_all add: fresh_def supp_finite_atom_set a)
-  done
+  by (auto dest!: aux_fresh)
+     (simp_all add: fresh_def supp_finite_atom_set a)
 
 lemma supp_abs_subset2:
   assumes a: "finite (supp x)"
   shows "supp (Abs as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
-  apply(rule_tac [!] supp_is_subset)
-  apply(simp_all add: abs_supports a)
-  done
+  by (rule_tac [!] supp_is_subset)
+     (simp_all add: abs_supports a)
 
 lemma abs_finite_supp:
   assumes a: "finite (supp x)"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] subset_antisym)
-  apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
-  done
+  by (rule_tac [!] subset_antisym)
+     (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
 
 lemma supp_abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] abs_finite_supp)
-  apply(simp_all add: finite_supp)
-  done
+  by (rule_tac [!] abs_finite_supp)
+     (simp_all add: finite_supp)
 
 instance abs_gen :: (fs) fs
   apply(default)