1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Jun 22 13:15:52 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Jun 22 14:34:06 2019 +0200
     1.3 @@ -8,11 +8,6 @@
     1.4  theory DiophantEq imports Base_Tools Equation Test
     1.5  begin
     1.6  
     1.7 -consts
     1.8 -  Diophant'_equation :: "[bool, int, bool ] 
     1.9 -                                       => bool "
    1.10 -                    ("((Script Diophant'_equation (_ _ =))//(_))" 9)
    1.11 -
    1.12  axiomatization where
    1.13    int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
    1.14  
    1.15 @@ -46,12 +41,7 @@
    1.16            ("#Find"  ,["boolTestFind s_s"])],
    1.17          {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
    1.18            crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.19 -        @{thm diophant_equation.simps}
    1.20 -	    (*"Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.21 -          "(Repeat                                                          " ^
    1.22 -          "    ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
    1.23 -          "     (Try (Calculate ''PLUS'')) @@  " ^
    1.24 -          "     (Try (Calculate ''TIMES''))) e_e::bool)"*))]
    1.25 +        @{thm diophant_equation.simps})]
    1.26  \<close>
    1.27  
    1.28  end
    1.29 \ No newline at end of file