1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Tue Aug 31 16:38:22 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Wed Sep 01 09:56:09 2010 +0200
     1.3 @@ -7,13 +7,23 @@
     1.4  *)
     1.5  
     1.6  theory Atools imports Descript 
     1.7 -uses ("../Interpret/mstools.sml") 
     1.8 -     ("../Interpret/ctree.sml")
     1.9 -     ("../Interpret/ptyps.sml") (*^^^ all for: fun prep_pbt, fun store_pbt*)
    1.10 +uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")
    1.11 +("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
    1.12 +("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
    1.13 +("Interpret/inform.sml")("Interpret/mathengine.sml")
    1.14 +
    1.15  begin
    1.16 -use "../Interpret/mstools.sml"
    1.17 -use "../Interpret/ctree.sml"
    1.18 -use "../Interpret/ptyps.sml"
    1.19 +use "Interpret/mstools.sml"
    1.20 +use "Interpret/ctree.sml"
    1.21 +use "Interpret/ptyps.sml"   (*^^^ use for: fun prep_pbt, fun store_pbt*)
    1.22 +use "Interpret/generate.sml"
    1.23 +use "Interpret/calchead.sml"
    1.24 +use "Interpret/appl.sml"
    1.25 +use "Interpret/rewtools.sml"
    1.26 +use "Interpret/script.sml"
    1.27 +use "Interpret/solve.sml"
    1.28 +use "Interpret/inform.sml"  (*^^^ use for: fun castab*)
    1.29 +use "Interpret/mathengine.sml"
    1.30  
    1.31  consts
    1.32  
    1.33 @@ -661,10 +671,10 @@
    1.34  		Calc ("Atools.occurs'_in",eval_occurs_in ""),    
    1.35  		Calc ("Tools.matches",eval_matches "")
    1.36  	       ],
    1.37 -      scr = Script ((term_of o the o (parse thy)) 
    1.38 +      scr = Script ((term_of o the o (parse @{theory})) 
    1.39        "empty_script")
    1.40        }:rls);
    1.41 -ruleset' := overwritelth thy 
    1.42 +ruleset' := overwritelth @{theory} 
    1.43  		(!ruleset',
    1.44  		 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
    1.45  		  ]);

     2.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Tue Aug 31 16:38:22 2010 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Wed Sep 01 09:56:09 2010 +0200
     2.3 @@ -19,36 +19,38 @@
     2.4    SimplifyScript      :: "[real,  real] => real"
     2.5                    ("((Script SimplifyScript (_ =))// (_))" 9)
     2.6  
     2.7 +ML {* "ok" *}
     2.8 +
     2.9  ML {*
    2.10  
    2.11  (** problems **)
    2.12  store_pbt
    2.13 - (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID
    2.14 + (prep_pbt @{theory} "pbl_simp" [] e_pblID
    2.15   (["simplification"],
    2.16 -  [("#Given" ,["TERM t_"]),
    2.17 -   ("#Find"  ,["normalform n_"])
    2.18 +  [("#Given" ,["TERM t_t"]),
    2.19 +   ("#Find"  ,["normalform n_n"])
    2.20    ],
    2.21    append_rls "e_rls" e_rls [(*for preds in where_*)], 
    2.22 -  SOME "Simplify t_", 
    2.23 +  SOME "Simplify t_t", 
    2.24    []));
    2.25  
    2.26  store_pbt
    2.27 - (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID
    2.28 + (prep_pbt @{theory} "pbl_vereinfache" [] e_pblID
    2.29   (["vereinfachen"],
    2.30 -  [("#Given" ,["TERM t_"]),
    2.31 -   ("#Find"  ,["normalform n_"])
    2.32 +  [("#Given" ,["TERM t_t"]),
    2.33 +   ("#Find"  ,["normalform n_n"])
    2.34    ],
    2.35    append_rls "e_rls" e_rls [(*for preds in where_*)], 
    2.36 -  SOME "Vereinfache t_", 
    2.37 +  SOME "Vereinfache t_t", 
    2.38    []));
    2.39  
    2.40  (** methods **)
    2.41  
    2.42  store_met
    2.43 -    (prep_met (theory "Simplify") "met_simp" [] e_metID
    2.44 +    (prep_met @{theory} "met_tsimp" [] e_metID
    2.45  	      (["simplification"],
    2.46 -	       [("#Given" ,["TERM t_"]),
    2.47 -		("#Find"  ,["normalform n_"])
    2.48 +	       [("#Given" ,["TERM t_t"]),
    2.49 +		("#Find"  ,["normalform n_n"])
    2.50  		],
    2.51  	       {rew_ord'="tless_true",
    2.52  		rls'= e_rls, 
    2.53 @@ -64,23 +66,23 @@
    2.54  (*.function for handling the cas-input "Simplify (2*a + 3*a)":
    2.55     make a model which is already in ptree-internal format.*)
    2.56  (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
    2.57 -   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    2.58 +   val (h,argl) = strip_comb ((term_of o the o (parse (theory "Simplify"))) 
    2.59  				  "Simplify (2*a + 3*a)");
    2.60     *)
    2.61  fun argl2dtss t =
    2.62 -    [((term_of o the o (parse thy)) "TERM", t),
    2.63 -     ((term_of o the o (parse thy)) "normalform", 
    2.64 -      [(term_of o the o (parse thy)) "N"])
    2.65 +    [((term_of o the o (parse @{theory})) "TERM", t),
    2.66 +     ((term_of o the o (parse @{theory})) "normalform", 
    2.67 +      [(term_of o the o (parse @{theory})) "N"])
    2.68       ]
    2.69    | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
    2.70  
    2.71  castab := 
    2.72  overwritel (!castab, 
    2.73 -	    [((term_of o the o (parse thy)) "Simplify",  
    2.74 -	      (("Isac.thy", ["simplification"], ["no_met"]), 
    2.75 +	    [((term_of o the o (parse @{theory})) "Simplify",  
    2.76 +	      (("Isac", ["simplification"], ["no_met"]), 
    2.77  	       argl2dtss)),
    2.78 -	     ((term_of o the o (parse thy)) "Vereinfache",  
    2.79 -	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 
    2.80 +	     ((term_of o the o (parse @{theory})) "Vereinfache",  
    2.81 +	      (("Isac", ["vereinfachen"], ["no_met"]), 
    2.82  	       argl2dtss))
    2.83  	     ]);
    2.84  *}