1.  
  2. (* We represent variables as strings containing a name *)
  3. type variable = string;
  4.  
  5. (* equality on variable names *)
  6. fun eqVar (v0:variable) (v1:variable) = (v0 = v1);
  7.  
  8. (* Formulas are either... *)
  9. datatype formula = 
  10. 	 True                          (* boolean True *)
  11.        | False                         (* boolean False *)
  12.        | Var of variable               (* a simple variable *)
  13.        | Not of formula                (* a negation of a single formula *)
  14.        | And of (formula list)         (* a conjunction of several formulas *)
  15.        | Or of (formula list)          (* a disjunction of several formulas *)
  16.        | Implies of formula * formula; (* an implication between one formula
  17.                                         * and another *)