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.
updated for 2014 release
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 08 Jul 2014 11:18:31 +0100
changeset 3238 b2e1a7b83e05
parent 3237 8ee8f72778ce
child 3239 67370521c09c
updated for 2014 release
Tutorial/Tutorial5.thy file | annotate | diff | comparison | revisions 
--- a/Tutorial/Tutorial5.thy	Mon Jul 07 10:21:40 2014 +0100
+++ b/Tutorial/Tutorial5.thy	Tue Jul 08 11:18:31 2014 +0100
@@ -128,9 +128,8 @@
 using ty fc
 apply(cases)
 using [[simproc del: alpha_lst]]
-apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
 apply(auto simp add: Abs1_eq_iff)
-apply(rotate_tac 3)
+apply(rotate_tac 4)
 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
 apply(auto simp add: flip_fresh_fresh ty_fresh)
nominal2