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.
Use eqvt.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 15 Mar 2010 09:27:25 +0100
changeset 1441 14b850159df1
parent 1440 ffd5540ac2e9
child 1442 097b25706436
Use eqvt.
Nominal/Test.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Test.thy	Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 09:27:25 2010 +0100
@@ -35,13 +35,7 @@
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: lam_bp_bn lam_bp_perm)
-apply(simp add: eqvts)
-done
+  by (rule eqvts)
 
 lemma supp_fv:
   "supp t = fv_lam t" and
nominal2