diff -r 6aa90baf7780 -r ca6aac81b893 src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Mar 14 16:50:44 2011 +0100
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Mar 17 10:11:18 2011 +0100
@@ -1,20 +1,24 @@
-theory DiophantEq imports Atools Equation begin
+(* Title:  Knowledge/DiophantEq.thy
+   Author: Mathias Lehnfeld 2011
+   (c) due to copyright terms
+12345678901234567890123456789012345678901234567890123456789012345678901234567890
+        10        20        30        40        50        60        70        80
+*)
+
+theory DiophantEq imports Atools Equation Test
+begin
 
 consts
-   Solve'_lineq'_equation :: "[bool, int, bool ] 
+  Diophant'_equation :: "[bool, int, bool ] 
                                        => bool "
                     ("((Script Diophant'_equation (_ _ =))//(_))" 9)
 axioms
 
-  int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"
+  int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
 
-ML {*
-val thy = @{theory};
-val ctxt = ProofContext.init_global thy;
-fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);
-parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)
-*}
+ML {*val thy = @{theory}*}
 
+text {*problemclass for the usecase*}
 ML {*
 store_pbt
  (prep_pbt thy "pbl_equ_dio" [] e_pblID
@@ -30,21 +34,24 @@
 get_pbt ["diophantine","equation"];
 *}
 
+text {*method solving the usecase*}
 ML {*
-val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
-val t = parseNEW ctxt "x + 1 = (2::int)";
-*} 
-
-ML {*
-rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
-
- 
-*}
-
-ML {*
-prop_of (@{thm "int_isolate_add"});
-writeln "-----------";
-t;
+store_met
+(prep_met thy "met_test_diophant" [] e_metID
+ (["Test","solve_diophant"]:metID,
+  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
+  (*                                      TODO: drop ^^^^^*)
+   ("#Where" ,[]),
+   ("#Find"  ,["boolTestFind s_s"]) 
+  ],
+   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
+    prls = e_rls, calc = [], crls = tval_rls, nrls = Test_simplify},
+ "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
+ "(Repeat                                                          " ^
+ "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
+ "     (Try (Calculate PLUS)) @@  " ^
+ "     (Try (Calculate TIMES))) e_e::bool)"
+ ))
 *}
 
 end
\ No newline at end of file