--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normif	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts normif :: ifex => ifex => ifex => ifex
+primrec
+"normif (CIF b)    t e = IF (CIF b) t e"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"