1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed May 16 08:59:09 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed May 16 15:01:47 2012 +0200
     1.3 @@ -631,17 +631,6 @@
     1.4  		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end
     1.5    end;
     1.6  
     1.7 -(* error patterns and fill patterns *)
     1.8 -type errpatID = string
     1.9 -type fillpatID = string
    1.10 -type errpat =
    1.11 -  errpatID    (* one identifier for a list of patterns *)
    1.12 -  * term list (* error patterns                        *)
    1.13 -  * thm list  (* thms related to error patterns;
    1.14 -                 note that respective lhs do not match
    1.15 -                 (which reflects student's error)      *)
    1.16 -val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
    1.17 -
    1.18  (* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
    1.19  fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
    1.20    let 

     2.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Wed May 16 08:59:09 2012 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Wed May 16 15:01:47 2012 +0200
     2.3 @@ -291,6 +291,17 @@
     2.4      pair2str (field, pair2str (term2str dsc, term2str id));
     2.5  fun pats2str pats = (strs2str o (map pat2str)) pats;
     2.6  
     2.7 +(* error patterns and fill patterns *)
     2.8 +type errpatID = string
     2.9 +type fillpatID = string
    2.10 +type errpat =
    2.11 +  errpatID    (* one identifier for a list of patterns                       *)
    2.12 +  * term list (* error patterns                                              *)
    2.13 +  * thm list  (* thms related to error patterns; note that respective lhs 
    2.14 +                 do not match (which reflects student's error).
    2.15 +                 fillpatterns are stored with these thms.                    *)
    2.16 +val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
    2.17 +
    2.18  (* data for methods stored in 'methods'-database *)
    2.19  type met = 
    2.20       {guh        : guh,        (*unique within this isac-knowledge           *)
    2.21 @@ -304,44 +315,22 @@
    2.22        prls       : rls,        (*for evaluating predicates in modelpattern   *)
    2.23        crls       : rls,        (*for check_elementwise, ie. formulae in calc.*)
    2.24        nrls       : rls,        (*canonical simplifier specific for this met  *)
    2.25 +(*      errpats    : errpat list,(*error patterns expected in this method      *)*)
    2.26        calc       : calc list,  (*040207: <--- calclist' in fun prep_met      *)
    2.27        (*branch   : TransitiveB set in append_problem at generation ob pblobj
    2.28 -       FIXXXME.0308: set branch from met in Apply_Method ?                   *)
    2.29 -
    2.30 -      (* compare type pbt:*)
    2.31 -      ppc: pat list,       
    2.32 -      (*.items in given, find, relate;
    2.33 -	items (in "#Find") which need not occur in the arg-list of a SubProblem
    2.34 -        are 'copy-named' with an identifier "*_!_".
    2.35 -        copy-named items are 'generating' if they are NOT "*___"
    2.36 -        see ME/calchead.sml 'fun is_copy_named'.*)
    2.37 -      pre: term list,          (*preconditions in where*)
    2.38 -      (*script*)  
    2.39 -      scr: scr (*prep_met requires either script or string "empty_script"*)
    2.40 +          FIXXXME.0308: set branch from met in Apply_Method ?                *)
    2.41 +      ppc        : pat list,   (*.items in given, find, relate;
    2.42 +	      items (in "#Find") which need not occur in the arg-list of a SubProblem
    2.43 +        are 'copy-named' with an identifier "*'.'".
    2.44 +        copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
    2.45 +        see ME/calchead.sml 'fun is_copy_named'.                              *)
    2.46 +      pre        : term list,  (*preconditions in where                       *)
    2.47 +      scr        : scr         (*prep_met gets progam or string "empty_script"*)
    2.48  	   };
    2.49 -(* ------- template ------------------------------------------------------
    2.50 -store_met
    2.51 -    (prep_met *.thy
    2.52 -	      ([(*"EqSystem","normalize"*)],
    2.53 -	       [("#Given" ,[  (*"equalities es_", "solveForVars vs_"*)]),
    2.54 -		("#Find"  ,[  (*dont forget typing non-reals        *)]),
    2.55 -		("#Relate",[])(*may be omitted                      *)  ],
    2.56 -	       {calc = [],             (*filled autom. in prep_met      *)
    2.57 -		crls = Erls,           (*for check_elementwise          *)
    2.58 -		prls = Erls,           (*for evaluating preds in guard  *)
    2.59 -		nrls = Erls,           (*can.simplifier for all formulae*)
    2.60 -		rew_ord'="tless_true", (*for rules in Detail            *)
    2.61 -		rls' = Erls,     (*erls, the eval_rls for cond. in rules*)
    2.62 -		srls = Erls},          (*for evaluating list expr in scr*)
    2.63 -	       "empty_script"
    2.64 -	       ));
    2.65 ----------- template ----------------------------------------------------*)
    2.66  val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
    2.67  	     rew_ord' = "e_rew_ord'": rew_ord',
    2.68  	      erls = e_rls, srls = e_rls, prls = e_rls,
    2.69 -	      calc = [], crls = e_rls, nrls = e_rls,
    2.70 -	      (*asm_thm = []: thm' list,
    2.71 -	      asm_rls = []: rls' list,*)
    2.72 +	      calc = [], crls = e_rls, (*errpats = [],*) nrls= e_rls,
    2.73  	      ppc = []: (string * (term * term)) list,
    2.74  	      pre = []: term list,
    2.75  	      scr = EmptyScr: scr}:met;
    2.76 @@ -535,15 +524,6 @@
    2.77       ptyps:= insrt pblID pbt (rev pblID) (!ptyps));
    2.78  
    2.79  (*.the metID has the root-element as first; compare 'fun store_pbt'.*)
    2.80 -(* val (met as {guh,...}, metID) = 
    2.81 -       ((prep_met EqSystem.thy "met_eqsys" [] e_metID
    2.82 -	      (["EqSystem"],
    2.83 -	       [],
    2.84 -	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
    2.85 -		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
    2.86 -	       "empty_script"
    2.87 -	       )));
    2.88 -   *)
    2.89  fun store_met (met as {guh,...}, metID) =
    2.90      (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
    2.91       mets:= insrt metID met metID (!mets));
    2.92 @@ -654,7 +634,7 @@
    2.93  	     (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
    2.94      {rew_ord'=ro, rls'=rls, srls=srls, prls=prls, 
    2.95       calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
    2.96 -     crls=cr, nrls=nr}, scr) =
    2.97 +     crls=cr, (*errpats = ep,*) nrls= nr}, scr) =
    2.98      let fun eq f (f', _) = f = f';
    2.99  	(*val thy = (assoc_thy o fst) metID*)
   2.100  	val gi = filter (eq "#Given") ppc;
   2.101 @@ -713,7 +693,7 @@
   2.102  	 calc = if scr = "empty_script" then []
   2.103  		else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o 
   2.104  		      (filter is_calc) o stacpbls) sc, 
   2.105 -	 crls=cr, nrls=nr, scr=Script sc}:met,
   2.106 +	 crls=cr, (*errpats = ep,*) nrls= nr, scr=Script sc}:met,
   2.107  	metID:metID)
   2.108      end;
   2.109  

     3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed May 16 08:59:09 2012 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Wed May 16 15:01:47 2012 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4   (["DiffApp"],
     3.5     [],
     3.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     3.7 -    crls = Atools_erls, nrls=norm_Rational
     3.8 +    crls = Atools_erls, nrls = norm_Rational
     3.9      (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
    3.10  *}
    3.11  ML{*
    3.12 @@ -163,7 +163,7 @@
    3.13      ("#Relate",[])
    3.14      ],
    3.15    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
    3.16 -    crls = eval_rls, nrls=norm_Rational
    3.17 +    crls = eval_rls, nrls = norm_Rational
    3.18     (*,  asm_rls=[],asm_thm=[]*)},
    3.19    "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)       " ^
    3.20    "      (v_v::real) (itv_v::real set) (e_rr::bool) =                       " ^ 
    3.21 @@ -189,7 +189,7 @@
    3.22      ("#Find"  ,["functionEq f_1"])
    3.23      ],
    3.24     {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
    3.25 -    calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
    3.26 +    calc=[], crls = eval_rls, nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
    3.27    "Script Make_fun_by_new_variable (f_f::real) (v_v::real)                " ^
    3.28    "      (eqs::bool list) =                                            " ^
    3.29    "(let h_h = (hd o (filterVar f_f)) eqs;                                " ^
    3.30 @@ -216,7 +216,7 @@
    3.31      ("#Find"  ,["functionEq f_1"])
    3.32      ],
    3.33     {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
    3.34 -    crls = eval_rls, nrls=norm_Rational
    3.35 +    crls = eval_rls, nrls = norm_Rational
    3.36      (*, asm_rls=[],asm_thm=[]*)},
    3.37     "Script Make_fun_by_explicit (f_f::real) (v_v::real)                 " ^
    3.38     "      (eqs::bool list) =                                         " ^
    3.39 @@ -239,7 +239,7 @@
    3.40      ("#Find"  ,["maxArgument v_0"])
    3.41      ],
    3.42     {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
    3.43 -    crls = eval_rls, nrls=norm_Rational
    3.44 +    crls = eval_rls, nrls = norm_Rational
    3.45      (*, asm_rls=[],asm_thm=[]*)},
    3.46     "empty_script"
    3.47     ));
    3.48 @@ -250,7 +250,7 @@
    3.49   (["DiffApp","find_values"]:metID,
    3.50     [],
    3.51     {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
    3.52 -    crls = eval_rls, nrls=norm_Rational(*,
    3.53 +    crls = eval_rls, nrls = norm_Rational(*,
    3.54      asm_rls=[],asm_thm=[]*)},
    3.55     "empty_script"));
    3.56  

     4.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Wed May 16 08:59:09 2012 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Wed May 16 15:01:47 2012 +0200
     4.3 @@ -85,7 +85,7 @@
     4.4   (["InsSort"],
     4.5     [],
     4.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     4.7 -    crls = Atools_rls, nrls=norm_Rational
     4.8 +    crls = Atools_rls, nrls = norm_Rational
     4.9      (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
    4.10  store_met
    4.11   (prep_met (Thy_Info.get_theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*)
    4.12 @@ -94,7 +94,7 @@
    4.13      ("#Find"  ,["sorted s_"])
    4.14      ],
    4.15     {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
    4.16 -    crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
    4.17 +    crls = eval_rls, nrls = norm_Rational},
    4.18     "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
    4.19    ));
    4.20  

     5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed May 16 08:59:09 2012 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed May 16 15:01:47 2012 +0200
     5.3 @@ -145,8 +145,7 @@
     5.4   (["LinEq"],
     5.5     [],
     5.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     5.7 -    crls=LinEq_crls, nrls=norm_Poly
     5.8 -    (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
     5.9 +    crls=LinEq_crls, nrls = norm_Poly}, "empty_script"));
    5.10  
    5.11  (* ansprechen mit ["LinEq","solve_univar_equation"] *)
    5.12  store_met
    5.13 @@ -158,7 +157,7 @@
    5.14      ("#Find",  ["solutions v_v'i'"])
    5.15     ],
    5.16     {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
    5.17 -    calc=[], crls=LinEq_crls, nrls=norm_Poly},
    5.18 +    calc=[], crls=LinEq_crls, nrls = norm_Poly},
    5.19      "Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    5.20      "(let e_e =((Try         (Rewrite      all_left           False)) @@   " ^ 
    5.21      "           (Try (Repeat (Rewrite     makex1_x            False))) @@  " ^ 

     6.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Wed May 16 08:59:09 2012 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Wed May 16 15:01:47 2012 +0200
     6.3 @@ -50,7 +50,7 @@
     6.4     ("#Find"  ,["solutions v_v'i'"])
     6.5    ],
     6.6     {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
     6.7 -    calc=[],crls=PolyEq_crls, nrls=norm_Rational},
     6.8 +    calc=[],crls=PolyEq_crls, nrls = norm_Rational},
     6.9      "Script Solve_log (e_e::bool) (v_v::real) =     " ^
    6.10      "(let e_e = ((Rewrite equality_power False) @@ " ^
    6.11      "           (Rewrite exp_invers_log False) @@ " ^

     7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed May 16 08:59:09 2012 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed May 16 15:01:47 2012 +0200
     7.3 @@ -1041,7 +1041,7 @@
     7.4   (["PolyEq"],
     7.5     [],
     7.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     7.7 -    crls=PolyEq_crls, nrls=norm_Rational}, "empty_script"));
     7.8 +    crls=PolyEq_crls, nrls = norm_Rational}, "empty_script"));
     7.9  
    7.10  store_met
    7.11   (prep_met thy "met_polyeq_norm" [] e_metID
    7.12 @@ -1056,7 +1056,7 @@
    7.13      srls=e_rls,
    7.14      prls=PolyEq_prls,
    7.15      calc=[],
    7.16 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.17 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.18      "Script Normalize_poly (e_e::bool) (v_v::real) =                     " ^
    7.19      "(let e_e =((Try         (Rewrite     all_left          False)) @@  " ^ 
    7.20      "          (Try (Repeat (Rewrite     makex1_x         False))) @@  " ^ 
    7.21 @@ -1083,7 +1083,7 @@
    7.22      srls=e_rls,
    7.23      prls=PolyEq_prls,
    7.24      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.25 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.26 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.27     "Script Solve_d0_polyeq_equation  (e_e::bool) (v_v::real)  = " ^
    7.28      "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]      " ^
    7.29      "                  d0_polyeq_simplify  False))) e_e        " ^
    7.30 @@ -1101,7 +1101,7 @@
    7.31    ],
    7.32     {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
    7.33      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.34 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.35 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.36     "Script Solve_d1_polyeq_equation  (e_e::bool) (v_v::real)  =   " ^
    7.37      "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^
    7.38      "                  d1_polyeq_simplify   True))          @@  " ^
    7.39 @@ -1125,7 +1125,7 @@
    7.40      srls=e_rls,
    7.41      prls=PolyEq_prls,
    7.42      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.43 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.44 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.45     "Script Solve_d2_polyeq_equation  (e_e::bool) (v_v::real) =      " ^
    7.46      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^
    7.47      "                    d2_polyeq_simplify           True)) @@   " ^
    7.48 @@ -1152,7 +1152,7 @@
    7.49      srls=e_rls,
    7.50      prls=PolyEq_prls,
    7.51      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.52 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.53 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.54     "Script Solve_d2_polyeq_bdvonly_equation  (e_e::bool) (v_v::real) =" ^
    7.55      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^
    7.56      "                   d2_polyeq_bdv_only_simplify    True)) @@  " ^
    7.57 @@ -1179,7 +1179,7 @@
    7.58      srls=e_rls,
    7.59      prls=PolyEq_prls,
    7.60      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.61 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.62 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.63     "Script Solve_d2_polyeq_sqonly_equation  (e_e::bool) (v_v::real) =" ^
    7.64      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]          " ^
    7.65      "                   d2_polyeq_sq_only_simplify     True)) @@   " ^
    7.66 @@ -1203,7 +1203,7 @@
    7.67      srls=e_rls,
    7.68      prls=PolyEq_prls,
    7.69      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.70 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.71 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.72     "Script Solve_d2_polyeq_pq_equation  (e_e::bool) (v_v::real) =   " ^
    7.73      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^
    7.74      "                   d2_polyeq_pqFormula_simplify   True)) @@  " ^
    7.75 @@ -1227,7 +1227,7 @@
    7.76      srls=e_rls,
    7.77      prls=PolyEq_prls,
    7.78      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.79 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.80 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.81     "Script Solve_d2_polyeq_abc_equation  (e_e::bool) (v_v::real) =   " ^
    7.82      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]          " ^
    7.83      "                   d2_polyeq_abcFormula_simplify   True)) @@  " ^
    7.84 @@ -1251,7 +1251,7 @@
    7.85      srls=e_rls,
    7.86      prls=PolyEq_prls,
    7.87      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.88 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.89 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.90     "Script Solve_d3_polyeq_equation  (e_e::bool) (v_v::real) =     " ^
    7.91      "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^
    7.92      "                    d3_polyeq_simplify           True)) @@  " ^
    7.93 @@ -1281,7 +1281,7 @@
    7.94    ],
    7.95     {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
    7.96      calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
    7.97 -    crls=PolyEq_crls, nrls=norm_Rational},
    7.98 +    crls=PolyEq_crls, nrls = norm_Rational},
    7.99     "Script Complete_square (e_e::bool) (v_v::real) =                         " ^
   7.100     "(let e_e = " ^ 
   7.101     "    ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^

     8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed May 16 08:59:09 2012 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed May 16 15:01:47 2012 +0200
     8.3 @@ -201,8 +201,7 @@
     8.4   (["RatEq"],
     8.5     [],
     8.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     8.7 -    crls=RatEq_crls, nrls=norm_Rational
     8.8 -    (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
     8.9 +    crls=RatEq_crls, nrls = norm_Rational}, "empty_script"));
    8.10  *}
    8.11  
    8.12  ML {*
    8.13 @@ -218,7 +217,7 @@
    8.14      srls=e_rls,
    8.15      prls=RatEq_prls,
    8.16      calc=[],
    8.17 -    crls=RatEq_crls, nrls=norm_Rational},
    8.18 +    crls=RatEq_crls, nrls = norm_Rational},
    8.19     "Script Solve_rat_equation  (e_e::bool) (v_v::real) =                   " ^
    8.20      "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
    8.21      "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^

     9.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Wed May 16 08:59:09 2012 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Wed May 16 15:01:47 2012 +0200
     9.3 @@ -530,8 +530,7 @@
     9.4   (["RootEq"],
     9.5     [],
     9.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     9.7 -    crls=RootEq_crls, nrls=norm_Poly(*,
     9.8 -    asm_rls=[],asm_thm=[]*)}, "empty_script"));
     9.9 +    crls=RootEq_crls, nrls = norm_Poly}, "empty_script"));
    9.10  
    9.11  (*-- normalize 20.10.02 --*)
    9.12  store_met
    9.13 @@ -545,7 +544,7 @@
    9.14      ("#Find"  ,["solutions v_v'i'"])
    9.15     ],
    9.16     {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
    9.17 -    calc=[], crls=RootEq_crls, nrls=norm_Poly},
    9.18 +    calc=[], crls=RootEq_crls, nrls = norm_Poly},
    9.19     "Script Norm_sq_root_equation  (e_e::bool) (v_v::real)  =                " ^
    9.20      "(let e_e = ((Repeat(Try (Rewrite     makex1_x            False))) @@  " ^
    9.21      "           (Try (Repeat (Rewrite_Set expand_rootbinoms  False))) @@  " ^ 
    9.22 @@ -571,7 +570,7 @@
    9.23      ("#Find"  ,["solutions v_v'i'"])
    9.24     ],
    9.25     {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
    9.26 -    prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
    9.27 +    prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls = norm_Poly},
    9.28  "Script Solve_sq_root_equation  (e_e::bool) (v_v::real)  =               " ^
    9.29  "(let e_e =                                                              " ^
    9.30  "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@      " ^
    9.31 @@ -628,7 +627,7 @@
    9.32      srls=e_rls,
    9.33      prls=RootEq_prls,
    9.34      calc=[],
    9.35 -    crls=RootEq_crls, nrls=norm_Poly},
    9.36 +    crls=RootEq_crls, nrls = norm_Poly},
    9.37      "Script Solve_left_sq_root_equation  (e_e::bool) (v_v::real)  =          " ^
    9.38      "(let e_e =                                                             " ^
    9.39      "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate  False)) @@ " ^

    10.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed May 16 08:59:09 2012 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed May 16 15:01:47 2012 +0200
    10.3 @@ -162,7 +162,7 @@
    10.4   (["RootRatEq"],
    10.5     [],
    10.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    10.7 -    crls=Atools_erls, nrls=norm_Rational}, "empty_script"));
    10.8 +    crls=Atools_erls, nrls = norm_Rational}, "empty_script"));
    10.9  (*-- left 20.10.02 --*)
   10.10  store_met
   10.11   (prep_met thy "met_rootrateq_elim" [] e_metID
   10.12 @@ -177,9 +177,7 @@
   10.13      srls=e_rls,
   10.14      prls=RootRatEq_prls,
   10.15      calc=[],
   10.16 -    crls=RootRatEq_crls, nrls=norm_Rational(*,
   10.17 -    asm_rls=[],
   10.18 -    asm_thm=[]*)},
   10.19 +    crls=RootRatEq_crls, nrls = norm_Rational},
   10.20     "Script Elim_rootrat_equation  (e_e::bool) (v_v::real)  =      " ^
   10.21      "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@  " ^ 
   10.22      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^ 

    11.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed May 16 08:59:09 2012 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed May 16 15:01:47 2012 +0200
    11.3 @@ -596,8 +596,7 @@
    11.4   (["Test"],
    11.5     [],
    11.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    11.7 -    crls=Atools_erls, nrls=e_rls(*,
    11.8 -    asm_rls=[],asm_thm=[]*)}, "empty_script"));
    11.9 +    crls=Atools_erls, nrls = e_rls}, "empty_script"));
   11.10  *}
   11.11  ML {*
   11.12  store_met
   11.13 @@ -916,7 +915,7 @@
   11.14     prls =append_rls "prls_contains_root" e_rls 
   11.15  		    [Calc ("Test.contains'_root",eval_contains_root "")],
   11.16     calc=[],
   11.17 -   crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.18 +   crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.19     asm_thm=[("square_equation_left",""),
   11.20  	    ("square_equation_right","")]*)},
   11.21   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.22 @@ -948,7 +947,7 @@
   11.23     srls = append_rls "srls_contains_root" e_rls 
   11.24  		     [Calc ("Test.contains'_root",eval_contains_root"")],
   11.25     prls=e_rls,calc=[],
   11.26 -   crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.27 +   crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.28     asm_thm=[("square_equation_left",""),
   11.29  	    ("square_equation_right","")]*)},
   11.30   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.31 @@ -982,7 +981,7 @@
   11.32    {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
   11.33     prls = append_rls "prls_met_test_squ_sub" e_rls
   11.34       [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
   11.35 -   calc=[], crls=tval_rls, nrls=Test_simplify},
   11.36 +   calc=[], crls=tval_rls, nrls = Test_simplify},
   11.37    "Script Solve_root_equation (e_e::bool) (v_v::real) =       " ^
   11.38    " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@    " ^
   11.39    "            (Try (Rewrite_Set Test_simplify False))) e_e;  " ^
   11.40 @@ -1004,7 +1003,7 @@
   11.41     ("#Find"  ,["solutions v_v'i'"])
   11.42     ],
   11.43    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
   11.44 -    crls=tval_rls, nrls=e_rls(*,
   11.45 +    crls=tval_rls, nrls = e_rls(*,
   11.46     asm_rls=[],asm_thm=[("square_equation_left",""),
   11.47  	    ("square_equation_right","")]*)},
   11.48     "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.49 @@ -1027,7 +1026,7 @@
   11.50     srls = append_rls "srls_contains_root" e_rls 
   11.51  		     [Calc ("Test.contains'_root",eval_contains_root"")],
   11.52     prls=e_rls,calc=[],
   11.53 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.54 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.55     asm_thm=[("square_equation_left",""),
   11.56  	    ("square_equation_right","")]*)},
   11.57   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.58 @@ -1060,7 +1059,7 @@
   11.59     srls = append_rls "srls_contains_root" e_rls 
   11.60  		     [Calc ("Test.contains'_root",eval_contains_root"")],
   11.61     prls=e_rls,calc=[],
   11.62 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.63 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.64     asm_thm=[("square_equation_left",""),
   11.65  	    ("square_equation_right","")]*)},
   11.66   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.67 @@ -1092,7 +1091,7 @@
   11.68     srls = append_rls "srls_contains_root" e_rls 
   11.69  		     [Calc ("Test.contains'_root",eval_contains_root"")],
   11.70     prls=e_rls,calc=[],
   11.71 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.72 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.73     asm_thm=[("square_equation_left",""),
   11.74  	    ("square_equation_right","")]*)},
   11.75   "Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^
   11.76 @@ -1125,7 +1124,7 @@
   11.77     srls = append_rls "srls_contains_root" e_rls 
   11.78  		     [Calc ("Test.contains'_root",eval_contains_root"")],
   11.79     prls=e_rls,calc=[],
   11.80 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
   11.81 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
   11.82     asm_thm=[("square_equation_left",""),
   11.83  	    ("square_equation_right","")]*)},
   11.84   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
   11.85 @@ -1160,7 +1159,7 @@
   11.86     ],
   11.87     {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
   11.88      prls = assoc_rls "matches",
   11.89 -    crls=tval_rls, nrls=e_rls(*,
   11.90 +    crls=tval_rls, nrls = e_rls(*,
   11.91      asm_rls=[],asm_thm=[]*)},
   11.92    "Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^
   11.93     " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@         " ^
   11.94 @@ -1183,7 +1182,7 @@
   11.95     ],
   11.96     {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
   11.97     calc=[],
   11.98 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
   11.99 +    crls=tval_rls, nrls = e_rls},
  11.100    "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
  11.101     " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@   " ^
  11.102     "            (Try (Rewrite_Set Test_simplify False))) e_e   " ^

    12.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Wed May 16 08:59:09 2012 +0200
    12.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Wed May 16 15:01:47 2012 +0200
    12.3 @@ -199,18 +199,12 @@
    12.4  fun calcs2xmlOLD j [] = ("":xml) (*TODO replace with 'strs2xml'*)
    12.5    | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
    12.6  
    12.7 -(* val (id, {guh,mathauthors,init,ppc,pre,scr,calc,
    12.8 -	     crls,erls,nrls,prls,srls,rew_ord'}) =
    12.9 -       (["Test", "solve_linear"],
   12.10 -	get_met ["Test", "solve_linear"]);
   12.11 -   *)
   12.12 -
   12.13  (*.format a method in xml for presentation on the method browser;
   12.14     new version with <KESTOREREF>s -- not used because linking
   12.15     requires elements (rls, calc, ...) to be reorganized.*)
   12.16  (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
   12.17  fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
   12.18 -			 crls,erls,nrls,prls,srls,rew_ord'}:met) =
   12.19 +			 crls,erls,(*errpats,*)nrls,prls,srls,rew_ord'}:met) =
   12.20      let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
   12.21  	val crls' = (#id o rep_rls) crls
   12.22  	val erls' = (#id o rep_rls) erls
   12.23 @@ -248,7 +242,7 @@
   12.24  (*.format a method in xml for presentation on the method browser;
   12.25     old version with 'dead' strings for rls, calc, ....*)
   12.26  fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
   12.27 -			 crls,erls,nrls,prls,srls,rew_ord'}:met) =
   12.28 +			 crls,erls,(*errpats,*)nrls,prls,srls,rew_ord'}:met) =
   12.29      "<NODECONTENT>\n" ^
   12.30      indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
   12.31      id2xml i id ^