sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, intermediate start-work-070517
authorwneuper
Wed, 02 Jan 2008 10:06:00 +0100
branchstart-work-070517
changeset 271a24f77e0ffad
parent 270 ea899ab566cf
child 272 a95383a1f758
sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, intermediate
src/sml/calcelems.sml
     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