anchor.diff:  *)
   
   /// System of tactics (slightly different from any traditional LCF method).
  +
   module NHol.tactics
   
   open FSharp.Compatibility.OCaml
  
positive.code: (*                                                                           *)
  (*   f(@) [A1@ |- g1@; ...; An@ |- gn@] = A@ |- g@                           *)
  (* ------------------------------------------------------------------------- *)
  
  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;;
  
  (* ------------------------------------------------------------------------- *)
  (* A goalstack is just a list of goalstates. Could go for more...            *)
  (* ------------------------------------------------------------------------- *)
  
  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;;
  
  (* ------------------------------------------------------------------------- *)
  (* A tactic, applied to a goal A ?- g, returns:                              *)
  
negative.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],       *)
  