1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 12:45:58 2011 +0100
1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 15:12:55 2011 +0100
1.3 @@ -32,11 +32,10 @@
1.4
1.5 ML {*
1.6 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
1.7 -val t = parseNEW ctxt "x + y = (y::int)";
1.8 +val t = parseNEW ctxt "x + 1 = (2::int)";
1.9 *}
1.10
1.11 ML {*
1.12 -tracing "\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>";
1.13 rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
1.14
1.15