equal
deleted
inserted
replaced
80 then SOME ((term2str p) ^ " = True", |
80 then SOME ((term2str p) ^ " = True", |
81 Trueprop $ (mk_equality (p, @{term True}))) |
81 Trueprop $ (mk_equality (p, @{term True}))) |
82 else SOME ((term2str p) ^ " = False", |
82 else SOME ((term2str p) ^ " = False", |
83 Trueprop $ (mk_equality (p, @{term False}))) |
83 Trueprop $ (mk_equality (p, @{term False}))) |
84 | eval_occur_exactly_in _ _ _ _ = NONE; |
84 | eval_occur_exactly_in _ _ _ _ = NONE; |
85 |
|
86 calclist':= |
|
87 overwritel (!calclist', |
|
88 [("occur_exactly_in", |
|
89 ("EqSystem.occur'_exactly'_in", |
|
90 eval_occur_exactly_in "#eval_occur_exactly_in_")) |
|
91 ]); |
|
92 |
|
93 *} |
85 *} |
94 setup {* KEStore_Elems.add_calcs |
86 setup {* KEStore_Elems.add_calcs |
95 [("occur_exactly_in", |
87 [("occur_exactly_in", |
96 ("EqSystem.occur'_exactly'_in", |
88 ("EqSystem.occur'_exactly'_in", |
97 eval_occur_exactly_in "#eval_occur_exactly_in_"))] *} |
89 eval_occur_exactly_in "#eval_occur_exactly_in_"))] *} |