# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1295735548 -32400
# Node ID 96f3ac5d11adc23cecb5deac2ab12e2b1eb6f2c1
# Parent  b9e2a66a317cf43fc13d8924599d368cf4d577e7
Missing val.simps

diff -r b9e2a66a317c -r 96f3ac5d11ad Tutorial/Tutorial5.thy
--- 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!