# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269668687 -3600
# Node ID 3c51fccbe98965434adda3246ecb7a3778c3a5b6
# Parent  2922b04d9545710f08ffafa897113eb1b95ae9e0# Parent  a99ae705b81115abf9df538a528ff5fb707053bc
merged

diff -r 2922b04d9545 -r 3c51fccbe989 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Mar 27 06:44:14 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 06:44:47 2010 +0100
@@ -54,22 +54,25 @@
 fun
   alpha_abs 
 where
+  [simp del]:
   "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
 fun
   alpha_abs_lst
 where
+  [simp del]:
   "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
 
 fun
   alpha_abs_res
 where
+  [simp del]:
   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
 notation
-  alpha_abs ("_ \<approx>abs _") and
-  alpha_abs_lst ("_ \<approx>abs'_lst _") and
-  alpha_abs_res ("_ \<approx>abs'_res _")
+  alpha_abs (infix "\<approx>abs" 50) and
+  alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+  alpha_abs_res (infix "\<approx>abs'_res" 50)
 
 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
@@ -208,7 +211,7 @@
   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)
+  apply(simp_all add: alphas_abs)
   apply(lifting alphas_abs)
   done