equal
deleted
inserted
replaced
28 "x orelse y" == "tror`x`y" |
28 "x orelse y" == "tror`x`y" |
29 "If b then e1 else e2 fi" == "Icifte`b`e1`e2" |
29 "If b then e1 else e2 fi" == "Icifte`b`e1`e2" |
30 defs |
30 defs |
31 TT_def "TT==Def True" |
31 TT_def "TT==Def True" |
32 FF_def "FF==Def False" |
32 FF_def "FF==Def False" |
33 neg_def "neg == flift2 not" |
33 neg_def "neg == flift2 Not" |
34 ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)" |
34 ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)" |
35 andalso_def "trand == (LAM x y.If x then y else FF fi)" |
35 andalso_def "trand == (LAM x y.If x then y else FF fi)" |
36 orelse_def "tror == (LAM x y.If x then TT else y fi)" |
36 orelse_def "tror == (LAM x y.If x then TT else y fi)" |
37 (* andalso, orelse are different from strict functions |
37 (* andalso, orelse are different from strict functions |
38 andalso_def "trand == flift1(flift2 o (op &))" |
38 andalso_def "trand == flift1(flift2 o (op &))" |