equal
deleted
inserted
replaced
1572 val SOME (tt, _) = factout_p_ thy t; |
1572 val SOME (tt, _) = factout_p_ thy t; |
1573 if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))" |
1573 if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))" |
1574 then () else error "rls chancel_p 3"; |
1574 then () else error "rls chancel_p 3"; |
1575 |
1575 |
1576 "--- with simpler ruleset"; |
1576 "--- with simpler ruleset"; |
1577 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p"); |
1577 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p"); |
1578 val der = Derive.do_one ctxt Atools_erls rules ro NONE tt; |
1578 val der = Derive.do_one ctxt Atools_erls rules ro NONE tt; |
1579 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1579 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1580 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1580 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1581 |
1581 |
1582 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*) |
1582 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*) |
1586 |
1586 |
1587 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1587 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1588 (TermC.str2term "(1 * a + 1 * b) * (1 * a + - 1 * b)"); |
1588 (TermC.str2term "(1 * a + 1 * b) * (1 * a + - 1 * b)"); |
1589 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1589 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1590 |
1590 |
1591 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p"); |
1591 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (get_rls @{context} "rev_rew_p"); |
1592 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1592 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1593 (TermC.str2term "(1 * a + - 1 * b) * (1 * a + - 1 * b)"); |
1593 (TermC.str2term "(1 * a + - 1 * b) * (1 * a + - 1 * b)"); |
1594 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1594 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*) |
1595 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*) |
1595 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*) |
1596 (*WN060829 ...postponed*) |
1596 (*WN060829 ...postponed*) |