equal
deleted
inserted
replaced
85 Isabelle now provides an ML infix operator for reverse function application: |
85 Isabelle now provides an ML infix operator for reverse function application: |
86 |
86 |
87 infix |>; |
87 infix |>; |
88 fun (x |> f) = f x; |
88 fun (x |> f) = f x; |
89 |
89 |
90 Using this, theory extension really becomes a plasure, e.g.: |
90 Using this, theory extension really becomes a pleasure, e.g.: |
91 |
91 |
92 FOL.thy |
92 FOL.thy |
93 |> add_consts |
93 |> add_consts |
94 [("nand", "[o, o] => o", NoSyn), |
94 [("nand", "[o, o] => o", NoSyn), |
95 ("#", "[o, o] => o", Infixl 30)] |
95 ("#", "[o, o] => o", Infixl 30)] |