theory example_1 imports Isac

 begin

 section{*Equation Solving*}

 text{*Setup equation, Calc Tree,\ldots*}

 ML {*

   val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", 

               "solveFor z", "solutions L"];                        

   val (dI',pI',mI') =

     ("Isac", 

       ["abcFormula","degree_2","polynomial","univariate","equation"],

       ["no_met"]);

 *}

 text{*Step through the Calculation*}

 ML {*

   val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

 *}

 ML{*

  f2str f;

  show_pt pt;

 *}

 end