Tips on getting your EML specifications through the EML system

1. Variables in axioms need to be quantified! Some papers on EML don't do this for the sake of readability, but the official definition of EML requires it so that's what the implementation requires.
2. Quantification is written Forall x => exp and Exists x => exp (and Exists_unique x => exp), with capitalized Forall and Exists. Papers on Extended ML use lower-case forall and exists but in the implementation there is a conflict with library functions List.exists and Listpair.exists.
3. Use Forall (x,y) => exp or Forall x => Forall y => exp rather than Forall x,y => exp, and similarly for Exists.
4. Use == (EML logical equality, with type 'a * 'a -> bool) rather than = (ML computational equality, with type ''a * ''a -> bool). The two kinds of equality coincide on types like bool and int where they are both defined. The negation of == is =/=.
5. Put a space between ? and : when writing things like fun f(x:int) = ? :int . The definition of identifiers in ML says that ?: is an identifier rather than ? followed by :.
6. Don't use the variable o. This is ML function composition and is declared as infix, which leads to confusing error messages. To cancel the infix status of o if you do use it as a variable, specifications should be preceded with nonfix o.