src/Tools/isac/Knowledge/DiophantEq.thy
changeset 59488 10a9e97e77c3
parent 59473 28b67cae58c3
child 59504 546bd1b027cc
     1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Dec 14 20:53:15 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Dec 20 18:02:25 2018 +0100
     1.3 @@ -40,9 +40,9 @@
     1.4            crls = tval_rls, errpats = [], nrls = Test_simplify},
     1.5          "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
     1.6            "(Repeat                                                          " ^
     1.7 -          "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
     1.8 -          "     (Try (Calculate PLUS)) @@  " ^
     1.9 -          "     (Try (Calculate TIMES))) e_e::bool)")]
    1.10 +          "    ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
    1.11 +          "     (Try (Calculate ''PLUS'')) @@  " ^
    1.12 +          "     (Try (Calculate ''TIMES''))) e_e::bool)")]
    1.13  \<close>
    1.14  
    1.15  end
    1.16 \ No newline at end of file