doc-src/Tutorial/Ifexpr/normif
changeset 5377 efb799c5ed3c
equal deleted inserted replaced
5376:60b31a24f1a6 5377:efb799c5ed3c
       
     1 consts normif :: ifex => ifex => ifex => ifex
       
     2 primrec
       
     3 "normif (CIF b)    t e = IF (CIF b) t e"
       
     4 "normif (VIF x)    t e = IF (VIF x) t e"
       
     5 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"