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/Let.thy
changeset 2559 add799cf0817
parent 2514 69780ae147f5
child 2560 82e37a4595c7 
--- a/Nominal/Ex/Let.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Let.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -42,7 +42,7 @@
   "permute_bn_raw"
 
 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
   apply (rule TrueI)+
nominal2