equal
deleted
inserted
replaced
15 |
15 |
16 |
16 |
17 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
17 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
18 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
18 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
19 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
19 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------"; |
20 val form = TermC.str2term "x + -2 ::real" |
20 val form = TermC.parse_test @{context} "x + -2 ::real" |
21 val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify; |
21 val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify; |
22 val ctxt = Proof_Context.init_global @{theory Test}; |
22 val ctxt = Proof_Context.init_global @{theory Test}; |
23 (*Rewrite.trace_on := false; (*true false*)*) |
23 (*Rewrite.trace_on := false; (*true false*)*) |
24 (** )val NONE = ( *isa*) |
24 (** )val NONE = ( *isa*) |
25 (**)val SOME (form', _) = (*isa2*) |
25 (**)val SOME (form', _) = (*isa2*) |