equal
deleted
inserted
replaced
1 (* Trace.trace_rewrite:= true; |
1 (* Rewrite.trace_on:= true; |
2 Trace.trace_rewrite:= false; |
2 Rewrite.trace_on:= false; |
3 |
3 |
4 method "sqrt-equ-test", _NOT_ "square-equation" |
4 method "sqrt-equ-test", _NOT_ "square-equation" |
5 *) |
5 *) |
6 |
6 |
7 |
7 |
544 |
544 |
545 (*.9.6.03 |
545 (*.9.6.03 |
546 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"; |
546 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"; |
547 val SOME (t',asm) = rewrite_set_ thy false rls t; |
547 val SOME (t',asm) = rewrite_set_ thy false rls t; |
548 UnparseC.term t'; |
548 UnparseC.term t'; |
549 > Trace.trace_rewrite:=true; |
549 > Rewrite.trace_on:=true; |
550 Trace.trace_rewrite:=false; |
550 Rewrite.trace_on:=false; |
551 *) |
551 *) |
552 |
552 |
553 (*me------------ |
553 (*me------------ |
554 val (mI,m) = nxt; val pos' as (p,p_) = p; |
554 val (mI,m) = nxt; val pos' as (p,p_) = p; |
555 |
555 |