1.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy	Thu Jun 21 20:48:36 2012 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy	Fri Aug 31 19:19:07 2012 +0200
     1.3 @@ -1,12 +1,4 @@
     1.4 -(* Title:  example_1
     1.5 -   Author: Jan Rocnik
     1.6 -   Description: The following Example can be used as an HOWTO on applying
     1.7 -                already implemented Subproblems. In example solving a
     1.8 -                linear equation.
     1.9 -   (c) copyright due to license terms.
    1.10 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.11 -        10        20        30        40        50        60        70        80
    1.12 -*)
    1.13 +
    1.14  
    1.15  theory example_1 imports Isac
    1.16  begin
    1.17 @@ -15,25 +7,15 @@
    1.18  text{*Setup equation, Calc Tree,\ldots*}
    1.19  
    1.20  ML {*
    1.21 -  val equation = "equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))";
    1.22 -  val expr = [ equation, "solveFor z",   "solutions L"];                                              (*specification*)
    1.23 -             (*equality, bound variable, identifier for solution*)
    1.24 -
    1.25 +  val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", 
    1.26 +              "solveFor z", "solutions L"];                        
    1.27    val (dI',pI',mI') =
    1.28      ("Isac", 
    1.29        ["abcFormula","degree_2","polynomial","univariate","equation"],
    1.30        ["no_met"]);
    1.31 -
    1.32  *}
    1.33  
    1.34 -text{*Possible Check if the equation matches the designated Method*}
    1.35 -       
    1.36 -ML {*
    1.37 -  match_pbl expr (get_pbt 
    1.38 -    ["abcFormula","degree_2","polynomial","univariate","equation"]);
    1.39 -*}
    1.40 -
    1.41 -text{*Step throuh the Calculation Tree*}
    1.42 +text{*Step through the Calculation*}
    1.43  
    1.44  ML {*
    1.45    val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];