103 rules = Empty_Prog}) |
103 rules = Empty_Prog}) |
104 --- Outer_Syntax.command 5 |
104 --- Outer_Syntax.command 5 |
105 \<close> ML \<open> |
105 \<close> ML \<open> |
106 Rule_Set.append_rules "empty" Rule_Set.empty [] |
106 Rule_Set.append_rules "empty" Rule_Set.empty [] |
107 \<close> |
107 \<close> |
108 text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*) |
108 text \<open> for testcode cf. 1c8263e775d4 |
|
109 (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*) |
109 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], |
110 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], |
110 rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set |
111 rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set |
111 |
112 |
112 (*Output from: problem pbl_bieg : "Biegelinien" = .. HERE*) |
113 (*Output from: problem pbl_bieg : "Biegelinien" = .. HERE*) |
113 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], |
114 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], |