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.
Missing val.simps
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sun, 23 Jan 2011 07:32:28 +0900
changeset 2698 96f3ac5d11ad
parent 2697 b9e2a66a317c
child 2700 e0391947b7da
Missing val.simps
Tutorial/Tutorial5.thy file | annotate | diff | comparison | revisions 
--- a/Tutorial/Tutorial5.thy	Sun Jan 23 07:17:35 2011 +0900
+++ b/Tutorial/Tutorial5.thy	Sun Jan 23 07:32:28 2011 +0900
@@ -132,7 +132,7 @@
   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
 using a
 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
-   (auto elim: canonical_tArr)
+   (auto elim: canonical_tArr simp add: val.simps)
 
 text {*
   Done! Congratulations!
nominal2