12 datatype program = datatype Rule_Def.program |
12 datatype program = datatype Rule_Def.program |
13 |
13 |
14 val id_rls: Rule_Def.rule_set -> string |
14 val id_rls: Rule_Def.rule_set -> string |
15 val id_rule: Rule_Def.rule -> string |
15 val id_rule: Rule_Def.rule -> string |
16 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool |
16 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool |
|
17 val rule2str: Rule_Def.rule -> string |
|
18 val rule2str': Rule_Def.rule -> string |
|
19 |
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
18 (*NONE*) |
21 (*NONE*) |
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
20 (*NONE*) |
|
21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
22 end |
24 end |
23 |
25 |
24 (**) |
26 (**) |
25 structure Rule(**): RULE(**) = |
27 structure Rule(**): RULE(**) = |
52 fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2 |
54 fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2 |
53 | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2 |
55 | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2 |
54 | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2 |
56 | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2 |
55 | eq_rule _ = false; |
57 | eq_rule _ = false; |
56 |
58 |
|
59 fun rule2str Rule_Def.Erule = "Erule" |
|
60 | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")" |
|
61 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
|
62 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
|
63 | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")"; |
|
64 fun rule2str' Rule_Def.Erule = "Erule" |
|
65 | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
|
66 | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
|
67 | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
|
68 | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")"; |
|
69 |
57 (**)end(**) |
70 (**)end(**) |