Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-15 16:31:35 -0800 (Tue, 15 Feb 2000)
Revision: 2883
Log message:
Enabled the "strict" rewriter mode.
In "strict" mode, <<lambda{x.'t}>> will only match terms where "t" does not contain
free occurences of "x" while <<lambda{x.'t['x]}>> will match any lambda expression.
In "relaxed" mode both redices will match any lambda expression.
This is done
1) To force rule authors to completely specify the binding structure
2) To allow rule authors to specify free variables restrictions easier
refiner/refiner/refine.ml, filter/boot/rewrite_boot.ml and theories/tactic/tactic_cache.ml
use the strict mode.
filter/base/filter_prog.ml uses relaxed mode for d.f. and compiles ml rewrites
using the strict mode
refiner/reflib/dform.ml, refiner/reflib/term_dtable.ml and refiner/reflib/term_match_table.ml
use the relaxed mode.
Please let me know if this change breaks something.