lookup : term -> 'a net -> 'a list
# let BASIC_REWRITE_CONV' = FIRST_CONV (map REWR_CONV (basic_rewrites()));; val ( BASIC_REWRITE_CONV' ) : conv =
# let rewr_net = let enter_thm th = enter (freesl(hyp th)) (lhs(concl th),REWR_CONV th) in itlist enter_thm (basic_rewrites()) empty_net;;
# lookup `(\x. x + 1) 2` rewr_net;; val it : (term -> thm) list = [] # lookup `T /\ T` rewr_net;; val it : (term -> thm) list = [ ; ; ]
# let BASIC_REWRITE_CONV tm = FIRST_CONV (lookup tm rewr_net) tm;; val ( BASIC_REWRITE_CONV ) : term -> conv =
# let tm = funpow 8 (fun x -> mk_conj(x,x)) `T`;; ... time (DEPTH_CONV BASIC_REWRITE_CONV) tm;; CPU time (user): 0.08 ... time (DEPTH_CONV BASIC_REWRITE_CONV') tm;; CPU time (user): 1.121 ...