anchor.diff:  /// General simplification with given strategy and simpset and theorems.
   let GEN_SIMPLIFY_CONV (strat : strategy) ss lev thl = 
       let ss' = itlist AUGMENT_SIMPSET thl ss
  -    TRY_CONV(strat ss' lev)
  +    TRY_CONV (strat ss' lev)
   
   /// General top-level simplification with arbitrary simpset.
  -let ONCE_SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV ONCE_DEPTH_SQCONV ss 1
  +let ONCE_SIMPLIFY_CONV ss = 
  +    GEN_SIMPLIFY_CONV ONCE_DEPTH_SQCONV ss 1
   
   /// General simplification at depth with arbitrary simpset.
  -let SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 3
  +let SIMPLIFY_CONV ss = 
  +    GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 3
   
   (* ------------------------------------------------------------------------- *)
   (* Simple but useful default version.                                        *)
   (* ------------------------------------------------------------------------- *)
   
   /// Simpset consisting of only the default rewrites and conversions.
  -let empty_ss = Simpset(empty_net, basic_prover, [], fun x y -> Choice.get <| mk_rewrites true x y)
  +let empty_ss = 
  +    Simpset(empty_net, basic_prover, [], fun x y -> Choice.get <| mk_rewrites true x y)
   
   /// Construct a straightforward simpset from a list of theorems.
   let basic_ss = 
  
positive.code: 
  open FSharp.Compatibility.OCaml
  open FSharp.Compatibility.OCaml.Num
  open ExtCore.Control
  
  open NHol
  open lib
  
negative.code:         Simpset(net'', basic_prover, [], rewmaker)
  
  /// Simplify a term repeatedly by conditional contextual rewriting.
  let SIMP_CONV thl = 
      SIMPLIFY_CONV (basic_ss []) thl
  
  /// Simplify a term repeatedly by conditional contextual rewriting, not using default simplications.
  let PURE_SIMP_CONV thl = 
      SIMPLIFY_CONV empty_ss thl
  
  /// Simplify a term once by conditional contextual rewriting.
  let ONCE_SIMP_CONV thl = 
      ONCE_SIMPLIFY_CONV (basic_ss []) thl
  
  /// Simplify conclusion of a theorem repeatedly by conditional contextual rewriting.
  let SIMP_RULE thl = 
      CONV_RULE (SIMP_CONV thl)
  
  /// Simplify conclusion of a theorem repeatedly by conditional contextual rewriting, not using default simplifications.
  let PURE_SIMP_RULE thl = 
      CONV_RULE (PURE_SIMP_CONV thl)
  
  /// Simplify conclusion of a theorem once by conditional contextual rewriting.
  let ONCE_SIMP_RULE thl = 
      CONV_RULE (ONCE_SIMP_CONV thl)
  
  /// Simplify a goal repeatedly by conditional contextual rewriting.
  let SIMP_TAC thl = 
      CONV_TAC (SIMP_CONV thl)
  
  /// Simplify a goal repeatedly by conditional contextual rewriting without default simplifications.
  let PURE_SIMP_TAC thl = 
      CONV_TAC (PURE_SIMP_CONV thl)
  
  /// Simplify conclusion of goal once by conditional contextual rewriting.
  let ONCE_SIMP_TAC thl = 
      CONV_TAC (ONCE_SIMP_CONV thl)
  
  /// Perform simplification of goal by conditional contextual rewriting using assumptions and
  /// built-in simplifications.
  let ASM_SIMP_TAC = 
      ASM SIMP_TAC
  
  /// Perform simplification of goal by conditional contextual rewriting using assumptions.
  let PURE_ASM_SIMP_TAC = 
      ASM PURE_SIMP_TAC
  
  /// Simplify toplevel applicable terms in goal using assumptions and context.
  let ONCE_ASM_SIMP_TAC = 
      ASM ONCE_SIMP_TAC
  
  (* ------------------------------------------------------------------------- *)
  (* Abbreviation tactics.                                                     *)
  