--- 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