anchor.diff:      (* Basic theorem destructors.                                                *)
       (* ------------------------------------------------------------------------- *)
   
  +    /// Breaks a theorem into assumption list and conclusion.
       let dest_thm(Sequent(asl, c)) = (asl, c)
  +    /// Returns the hypotheses of a theorem.
       let hyp(Sequent(asl, c)) = asl
  +    /// Returns the conclusion of a theorem.
       let concl(Sequent(asl, c)) = c
       (* ------------------------------------------------------------------------- *)
       (* Basic equality properties; TRANS is derivable but included for efficiency *)
       (* ------------------------------------------------------------------------- *)
   
  +    /// Returns theorem expressing reflexivity of equality.
       let REFL tm = Sequent([], safe_mk_eq tm tm)
       
  +    /// Uses transitivity of equality on two equational theorems.
       let TRANS (Sequent(asl1, c1)) (Sequent(asl2, c2)) = 
           match (c1, c2) with
           | Comb((Comb(Const("=", _), _) as eql), m1), Comb(Comb(Const("=", _), m2), r) when alphaorder m1 m2 = 0 -> 
  
positive.code:     (* A few bits of general derived syntax.                                     *)
      (* ------------------------------------------------------------------------- *)
  
      let rator tm = 
          match tm with
          | Comb(l, r) -> l
          | _ -> failwith "rator: Not a combination"
      
      let rand tm = 
          match tm with
          | Comb(l, r) -> r
  
negative.code:     (* Return all the defined constants with generic types.                      *)
      (* ------------------------------------------------------------------------- *)
  
      /// Returns a list of the constants currently dened.
      let constants() = !the_term_constants
  
      (* ------------------------------------------------------------------------- *)
      (* Gets type of constant if it succeeds.                                     *)
      (* ------------------------------------------------------------------------- *)
  
      /// Gets the generic type of a constant from the name of the constant.
      let get_const_type s = assoc s (!the_term_constants)
      
      (* ------------------------------------------------------------------------- *)
      (* Declare a new constant.                                                   *)
      (* ------------------------------------------------------------------------- *)
  
      /// Declares a new constant.
      let new_constant(name, ty) = 
          if can get_const_type name then failwith("new_constant: constant " + name + " has already been declared")
          else the_term_constants := (name, ty) :: (!the_term_constants)
  