112 {id: string, (* for trace_rewrite *) |
112 {id: string, (* for trace_rewrite *) |
113 preconds: term list, (* STILL UNUSED *) |
113 preconds: term list, (* STILL UNUSED *) |
114 rew_ord: rew_ord_T,(* for rules *) |
114 rew_ord: rew_ord_T,(* for rules *) |
115 erls: rule_set, (* for the conditions in rules *) |
115 erls: rule_set, (* for the conditions in rules *) |
116 srls: rule_set, (* for evaluation of Prog_Expr *) |
116 srls: rule_set, (* for evaluation of Prog_Expr *) |
117 calc: calc list, (* for Calculate in program, set by prep_rls' *) |
117 calc: calc list, (* for calculation in program, set by prep_rls' *) |
118 rules: rule list, |
118 rules: rule list, |
119 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *) |
119 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *) |
120 scr: program} (* DEPRECATED: intersteps are created on the fly now *) |
120 scr: program} (* DEPRECATED: intersteps are created on the fly now *) |
121 | Sequence of (* a sequence of rules to be tried only once *) |
121 | Sequence of (* a sequence of rules to be tried only once *) |
122 {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set, |
122 {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set, |