extend_basic_congs : thm list -> unit
# SIMP_CONV[] `x = 1 /\ x < 2`;; val it : thm = |- x = 1 /\ x < 2 <=> x = 1 /\ x < 2
# extend_basic_congs [TAUT `(p <=> p') ==> (p' ==> (q <=> q')) ==> (p /\ q <=> p' /\ q')`];; val it : unit = ()
# SIMP_CONV[] `x = 1 /\ x < 2`;; val it : thm = |- x = 1 /\ x < 2 <=> x = 1 /\ 1 < 2 # SIMP_CONV[ARITH] `x = 1 /\ x < 2`;; val it : thm = |- x = 1 /\ x < 2 <=> x = 1