sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, intermediate
1.1 --- a/src/sml/calcelems.sml Wed Jan 02 09:56:26 2008 +0100
1.2 +++ b/src/sml/calcelems.sml Wed Jan 02 10:06:00 2008 +0100
1.3 @@ -170,6 +170,7 @@
1.4 | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.5 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.6
1.7 +(*WN080102 compare eq_rule ?!?*)
1.8 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.9 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.10 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
1.11 @@ -458,8 +459,11 @@
1.12 raise error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.13
1.14 (*. are _atomic_ rules equal ?.*)
1.15 +(*WN080102 compare eqrule ?!?*)
1.16 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
1.17 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.18 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.19 + (*id_rls checks for Rls, Seq, Rrls*)
1.20 | eq_rule _ = false;
1.21
1.22 fun merge_rls _ Erls rls = rls