equal
deleted
inserted
replaced
11 eqtype calID |
11 eqtype calID |
12 eqtype errpatID |
12 eqtype errpatID |
13 type rew_ord' = string |
13 type rew_ord' = string |
14 type rew_ord_ = LibraryC.subst -> term * term -> bool |
14 type rew_ord_ = LibraryC.subst -> term * term -> bool |
15 type rew_ord = rew_ord' * rew_ord_ |
15 type rew_ord = rew_ord' * rew_ord_ |
16 type eval_fn = string -> term -> theory -> (string * term) option |
16 type eval_fn = string -> term -> Proof.context -> (string * term) option |
17 |
17 |
18 datatype rule_set = |
18 datatype rule_set = |
19 Empty |
19 Empty |
20 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
20 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
21 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set} |
21 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set} |
40 (**) |
40 (**) |
41 structure Rule_Def(**): RULE_DEFINITION(**) = |
41 structure Rule_Def(**): RULE_DEFINITION(**) = |
42 struct |
42 struct |
43 (**) |
43 (**) |
44 |
44 |
45 type eval_fn = string -> term -> theory -> (string * term) option; |
45 type eval_fn = string -> term -> Proof.context -> (string * term) option; |
46 |
46 |
47 type rew_ord' = string; |
47 type rew_ord' = string; |
48 type rew_ord_ = LibraryC.subst -> term * term -> bool; |
48 type rew_ord_ = LibraryC.subst -> term * term -> bool; |
49 type rew_ord = rew_ord' * rew_ord_; |
49 type rew_ord = rew_ord' * rew_ord_; |
50 |
50 |