anchor.diff:  open NHol
   open lib
   open fusion
  -//open fusion.Hol_kernel
  +open fusion.Hol_kernel
   open basics
  -//open nets
  +open nets
   open printer
   open preterm
   open parser
  
positive.code: 
  let PAIR_EXISTS_THM = 
      prove((parse_term @"?x. ?(a:A) (b:B). x = mk_pair a b"), MESON_TAC [])
  let prod_tybij = 
      new_type_definition "prod" ("ABS_prod", "REP_prod") PAIR_EXISTS_THM
  let REP_ABS_PAIR = 
      prove
          ((parse_term 
  
negative.code: 
  let UNCURRY_DEF = 
      new_definition(parse_term @"!f x y. UNCURRY(f:A->B->C)(x,y) = f x y")
  
  let PASSOC_DEF = 
      new_definition
          (parse_term @"!f x y z. PASSOC (f:(A#B)#C->D) (x,y,z) = f ((x,y),z)")
  