# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268643739 -3600
# Node ID 097b257064362a498e855f32c66f79c90e887d78
# Parent  14b850159df13d1dc83f84c6ff86e95518ed554a
Prove alpha_gen_compose_eqvt

diff -r 14b850159df1 -r 097b25706436 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 15 09:27:25 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 15 10:02:19 2010 +0100
@@ -110,7 +110,10 @@
   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
-  oops
+  apply(simp add: c[symmetric])
+  apply(subst permute_eqvt[symmetric])
+  apply simp
+  done
 
 fun
   alpha_abs