Old: declare sort Nat New: declare sort Nat declare operator 0: -> nat declare operator 0: -> Nat
(Fewer parentheses are needed now because the boolean operators /\ and \/ bind more tightly than =>, which binds more tightly than <=>.)Old: not, &, | New: ~, /\, \/
Old: x + 0 == x New: x + 0 = x init(x) == x = 0 init(x) <=> x = 0 init(x) == x = 0 init(x) = (x = 0)
Old: declare op +: N, N -> N New: declare op __+__: N, N -> N
Old: assert ac + New: assert assert ac +; 1 = s(0) 1 = s(0); x + 0 = x x + 0 = x .. ..
Old: assert Nat generated by 0, s New: assert sort Nat generated by 0, s assert Set parititioned by /in assert sort Set partitioned by \in
Old: assert a.b:S = 2 New: assert a.(b:S) = 2 assert a:S[n] assert (a:S)[n]
Old: resume by case a b not(a | b) New: resume by case a, b, ~(a \/ b)
Old: when h1 h2 yield c1 c2 New: when h1, h2 yield c1, c2
Old: when forall x p(x) q(x) New: when \A x p(x), \A x q(x) yield c yield c
Old: display d-r nat set New: display d-r / (nat, set)
Old: prove P(x) by case x = 0 New: prove P(x) by case x = 0 <> 2 subgoals for proof <> case xc = 0 ... commands ... ... commands ... [] case 0 = xc [] case xc = 0 ... commands ... <> case ~(xc = 0) [] case not(0 = xc) ... commands ... [] conjecture [] case ~(xc = 0) [] conjecture