equal
deleted
inserted
replaced
422 fun ketype2str' Exp_ = "Example" |
422 fun ketype2str' Exp_ = "Example" |
423 | ketype2str' Thy_ = "Theory" |
423 | ketype2str' Thy_ = "Theory" |
424 | ketype2str' Pbl_ = "Problem" |
424 | ketype2str' Pbl_ = "Problem" |
425 | ketype2str' Met_ = "Method"; |
425 | ketype2str' Met_ = "Method"; |
426 |
426 |
427 (*see 'How to manage theorys in subproblems' at 'type thyID'*) |
|
428 val theory' = Unsynchronized.ref ([]:(theory' * theory) list); |
|
429 |
|
430 (*rewrite orders, also stored in 'type met' and type 'and rls' |
427 (*rewrite orders, also stored in 'type met' and type 'and rls' |
431 The association list is required for 'rewrite.."rew_ord"..' |
428 The association list is required for 'rewrite.."rew_ord"..' |
432 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
429 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
433 val rew_ord' = Unsynchronized.ref |
430 val rew_ord' = Unsynchronized.ref |
434 ([]:(rew_ord' * (*the key for the association list *) |
431 ([]:(rew_ord' * (*the key for the association list *) |