Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/LetRecB.thy
changeset 2922 a27215ab674e
parent 2920 99069744ad74
child 2950 0911cb7bf696 
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:45:30 2011 +0900
+++ b/Nominal/Ex/LetRecB.thy	Wed Jun 29 00:48:50 2011 +0100
@@ -181,6 +181,11 @@
   apply (simp add: eqvt_at_def)
   apply (simp add: eqvt_at_def)
 --""
+  apply(simp_all add: eqvt_def inj_on_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(perm_simp)
+  apply(simp)
   done
 
 termination by lexicographic_order
nominal2