1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Mon Nov 21 12:47:02 2016 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Tue Nov 22 10:42:21 2016 +0100
     1.3 @@ -1,7 +1,4 @@
     1.4 -(*
     1.5 -cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
     1.6 -/usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
     1.7 -*)
     1.8 +(* this is evaluated BEFORE Test_Isac.thu opens structures*)
     1.9  
    1.10  theory T3_MathEngine imports Isac begin
    1.11  
    1.12 @@ -63,7 +60,7 @@
    1.13    So we can start testing the example by calling 'CalcTreeTEST':
    1.14  *}
    1.15  ML {* val (p,_,f,nxt,_,pt) = 
    1.16 -      CalcTreeTEST 
    1.17 +      Math_Engine.CalcTreeTEST 
    1.18          [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
    1.19             "normalform N"],
    1.20  	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],
    1.21 @@ -90,18 +87,18 @@
    1.22    Only note the tactic 'nxt' suggested for the next step:
    1.23  *}
    1.24  ML {* val c = [(*this is an unimportant, but necessary detail*)];
    1.25 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.26 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.27 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.28 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.29  *}
    1.30  text{* The tactics 'Add_Given' and 'Add_Find' inserted the respective values
    1.31    into the model. Then 'Specify_Theory' determines the knowledge item no.1 from
    1.32    above, 'Specify_Problem' item 2 and 'Specify_Method' item 3.
    1.33  *}
    1.34  ML {* 
    1.35 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.36 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.37 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.38 -  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.39 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.40 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.41 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.42 +  val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
    1.43  *}
    1.44  text{* The final suggestion 'Apply_Method' completes the specification phase
    1.45    and starts the 'solving phase', which is guided by the method determined.
    1.46 @@ -116,10 +113,10 @@
    1.47    term at the end:
    1.48  *}
    1.49  ML {* default_print_depth 40; *}
    1.50 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    1.51 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    1.52 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    1.53 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    1.54 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    1.55 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    1.56 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    1.57 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    1.58  ML {* default_print_depth 3; *}
    1.59  text{* And, please, note that the result of applying the 'nxt' ruleset is to be
    1.60    found in the output of the next step !
    1.61 @@ -130,7 +127,7 @@
    1.62    perfect mathematics engine has to prove the socalled 'postcondition' of the
    1.63    current problem; this is not yet implemented in the current version of ISAC.
    1.64  *}
    1.65 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    1.66 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    1.67  text{* Now the mathematics engine has found the end of the calculation.
    1.68  
    1.69    With 'show_pt' the calculation can be inspected (in a more or less readable
    1.70 @@ -144,12 +141,12 @@
    1.71    the formalisation:
    1.72  *}
    1.73  ML {* val (p,_,f,nxt,_,pt) = 
    1.74 -      CalcTreeTEST 
    1.75 +      Math_Engine.CalcTreeTEST 
    1.76          [(["Term (1 + 2 + 3)", "normalform N"],
    1.77  	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],
    1.78  	           ["simplification","for_polynomials","with_minus"]))];
    1.79  *}
    1.80 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; *}
    1.81 +ML {* val (p,_,f,nxt,_,pt) =Math_Engine.me nxt p c pt; *}
    1.82  text{* and repeat this ML line as often as required ...*}
    1.83  
    1.84  end