Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove alpha_gen_compose_eqvt
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 15 Mar 2010 10:02:19 +0100
changeset 1442 097b25706436
parent 1441 14b850159df1
child 1443 d78c093aebeb
Prove alpha_gen_compose_eqvt
Nominal/Abs.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2