anchor.diff:  (*                                                                           *)
   (*   f(@) [A1@ |- g1@; ...; An@ |- gn@] = A@ |- g@                           *)
   (* ------------------------------------------------------------------------- *)
  -
  -type justification = instantiation -> thm list -> thm;;
  +type justification = instantiation -> thm list -> thm
   
   (* ------------------------------------------------------------------------- *)
   (* The goalstate stores the subgoals, justification, current instantiation,  *)
   (* and a list of metavariables.                                              *)
   (* ------------------------------------------------------------------------- *)
  -
  -type goalstate = (term list * instantiation) * goal list * justification;;
  +type goalstate = (term list * instantiation) * goal list * justification
   
   (* ------------------------------------------------------------------------- *)
   (* A goalstack is just a list of goalstates. Could go for more...            *)
   (* ------------------------------------------------------------------------- *)
  -
  -type goalstack = goalstate list;;
  +type goalstack = goalstate list
   
   (* ------------------------------------------------------------------------- *)
   (* A refinement, applied to a goalstate [A1 ?- g1; ...; An ?- gn]            *)
   (* yields a new goalstate with updated justification function, to            *)
   (* give a possibly-more-instantiated version of the initial goal.            *)
   (* ------------------------------------------------------------------------- *)
  -
  -type refinement = goalstate -> goalstate;;
  +type refinement = goalstate -> goalstate
   
   (* ------------------------------------------------------------------------- *)
   (* A tactic, applied to a goal A ?- g, returns:                              *)
  
positive.code: open bool
  open drule
  
  
  (* ------------------------------------------------------------------------- *)
  (* The common case of trivial instantiations.                                *)
  (* ------------------------------------------------------------------------- *)
  
  let null_inst = ([],[],[] :instantiation);;
  
  let null_meta = (([]:term list),null_inst);;
  
  (* ------------------------------------------------------------------------- *)
  (* A goal has labelled assumptions, and the hyps are now thms.               *)
  (* ------------------------------------------------------------------------- *)
  
  type goal = (string * thm) list * term;;
  
  let equals_goal ((a,w):goal) ((a',w'):goal) =
    forall2 (fun (s,th) (s',th') -> s = s' && equals_thm th th') a a' && w = w';;
  
  (* ------------------------------------------------------------------------- *)
  (* A justification function for a goalstate [A1 ?- g1; ...; An ?- gn],       *)
  
negative.code: *)
  
  /// System of tactics (slightly different from any traditional LCF method).
  
  module NHol.tactics
  
  open FSharp.Compatibility.OCaml
  