# HG changeset patch
# User nipkow
# Date 1160391091 -7200
# Node ID 14873e42659c1054b2863dd3fa7d8cc51d63802a
# Parent  24b8536dcf937666aa13d519e784ebfec3f455ed
added nbe_post for delayed_if

diff -r 24b8536dcf93 -r 14873e42659c src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:20:39 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:51:31 2006 +0200
@@ -118,6 +118,9 @@
 lemma [normal_pre]: "(if b then x else y) == delayed_if b (%u. x) (%u. y)"
 unfolding delayed_if_def by simp
 
+lemma [normal_post]: "delayed_if b f g == (if b then f() else g())"
+unfolding delayed_if_def by simp
+
 lemma [code func]:
  shows "delayed_if True f g = f()" and "delayed_if False f g = g()"
 by (auto simp:delayed_if_def)
@@ -127,4 +130,10 @@
 normal_form "OperationalEquality.eq [2..<4] [2,3]"
 (*lemma "OperationalEquality.eq [2..<4] [2,3]" by normalization*)
 
+definition
+ andalso :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+"andalso x y = (if x then y else False)"
+
+lemma "andalso a b = (if a then b else False)" by normalization
+
 end