equal
deleted
inserted
replaced
340 val script_thys = ref ([] : (theory' * theory) list); |
340 val script_thys = ref ([] : (theory' * theory) list); |
341 |
341 |
342 |
342 |
343 (*rewrite orders, also stored in 'type met' and type 'and rls' |
343 (*rewrite orders, also stored in 'type met' and type 'and rls' |
344 The association list is required for 'rewrite.."rew_ord"..' |
344 The association list is required for 'rewrite.."rew_ord"..' |
345 WN0509 tests not well-organized: see smltest/IsacKnowledge/termorder.sml*) |
345 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
346 val rew_ord' = |
346 val rew_ord' = |
347 ref ([]:(rew_ord' * (*the key for the association list *) |
347 ref ([]:(rew_ord' * (*the key for the association list *) |
348 (subst (*the bound variables - they get high order*) |
348 (subst (*the bound variables - they get high order*) |
349 -> (term * term) (*(t1, t2) to be compared *) |
349 -> (term * term) (*(t1, t2) to be compared *) |
350 -> bool)) (*if t1 <= t2 then true else false *) |
350 -> bool)) (*if t1 <= t2 then true else false *) |