1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Wed Jan 11 09:23:18 2023 +0100
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Wed Jan 11 11:38:01 2023 +0100
1.3 @@ -284,16 +284,16 @@
1.4 (* steps in rls d2_polyeq_bdv_only_simplify:*)
1.5
1.6 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
1.7 -t |> UnparseC.term; t |> TermC.atomty;
1.8 +t |> UnparseC.term; t |> TermC.atom_trace_detail @{context};
1.9 val thm = @{thm d2_prescind1};
1.10 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.11 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context};
1.12 val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
1.13
1.14 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
1.15 --> x = 0 | -6 + 5 * x = 0*)
1.16 -t' |> UnparseC.term; t' |> TermC.atomty;
1.17 +t' |> UnparseC.term; t' |> TermC.atom_trace_detail @{context};
1.18 val thm = @{thm d2_reduce_equation1};
1.19 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.20 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context};
1.21 val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
1.22 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.23 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"