Browse files

add simp rule for case expressions on lambdas

  • Loading branch information...
1 parent d37fdd2 commit 168ea6c033d5ae6c5fb96c3552dfa254eca77b8f Brian Huffman committed May 2, 2012
Showing with 1 addition and 1 deletion.
  1. +1 −1 isa/Halicore_Defs.thy
@@ -595,7 +595,7 @@ theorem Vcase_Vcon_Mwild:
shows "Vcase t (Vcon\<cdot>s\<cdot>xs) (\<lambda>w. Mwild (f w)) = f (Vcon\<cdot>s\<cdot>xs)"
using assms by (rule Vcase_Mwild) simp
-theorem Vcase_Vlam_Mwild:
+theorem Vcase_Vlam_Mwild [simp]:
assumes "cont f"
shows "Vcase t' (Vlam t g) (\<lambda>w. Mwild (f w)) = f (Vlam t g)"
using assms by (rule Vcase_Mwild, simp add: Vlam_def)

0 comments on commit 168ea6c

Please sign in to comment.