# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1283327769 -7200
# Node ID e0db2aedf2d46b14281851d02e9aa40e817e7bde
# Parent  bd4f7a35e892b69f677cd703d2d79c0c5d8184d3
updated Knowledge/Simplify

diff -r bd4f7a35e892 -r e0db2aedf2d4 src/Tools/isac/Knowledge/Atools.thy
--- a/src/Tools/isac/Knowledge/Atools.thy	Tue Aug 31 16:38:22 2010 +0200
+++ b/src/Tools/isac/Knowledge/Atools.thy	Wed Sep 01 09:56:09 2010 +0200
@@ -7,13 +7,23 @@
 *)
 
 theory Atools imports Descript 
-uses ("../Interpret/mstools.sml") 
-     ("../Interpret/ctree.sml")
-     ("../Interpret/ptyps.sml") (*^^^ all for: fun prep_pbt, fun store_pbt*)
+uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")
+("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
+("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
+("Interpret/inform.sml")("Interpret/mathengine.sml")
+
 begin
-use "../Interpret/mstools.sml"
-use "../Interpret/ctree.sml"
-use "../Interpret/ptyps.sml"
+use "Interpret/mstools.sml"
+use "Interpret/ctree.sml"
+use "Interpret/ptyps.sml"   (*^^^ use for: fun prep_pbt, fun store_pbt*)
+use "Interpret/generate.sml"
+use "Interpret/calchead.sml"
+use "Interpret/appl.sml"
+use "Interpret/rewtools.sml"
+use "Interpret/script.sml"
+use "Interpret/solve.sml"
+use "Interpret/inform.sml"  (*^^^ use for: fun castab*)
+use "Interpret/mathengine.sml"
 
 consts
 
@@ -661,10 +671,10 @@
 		Calc ("Atools.occurs'_in",eval_occurs_in ""),    
 		Calc ("Tools.matches",eval_matches "")
 	       ],
-      scr = Script ((term_of o the o (parse thy)) 
+      scr = Script ((term_of o the o (parse @{theory})) 
       "empty_script")
       }:rls);
-ruleset' := overwritelth thy 
+ruleset' := overwritelth @{theory} 
 		(!ruleset',
 		 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
 		  ]);
diff -r bd4f7a35e892 -r e0db2aedf2d4 src/Tools/isac/Knowledge/Simplify.thy
--- a/src/Tools/isac/Knowledge/Simplify.thy	Tue Aug 31 16:38:22 2010 +0200
+++ b/src/Tools/isac/Knowledge/Simplify.thy	Wed Sep 01 09:56:09 2010 +0200
@@ -19,36 +19,38 @@
   SimplifyScript      :: "[real,  real] => real"
                   ("((Script SimplifyScript (_ =))// (_))" 9)
 
+ML {* "ok" *}
+
 ML {*
 
 (** problems **)
 store_pbt
- (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID
+ (prep_pbt @{theory} "pbl_simp" [] e_pblID
  (["simplification"],
-  [("#Given" ,["TERM t_"]),
-   ("#Find"  ,["normalform n_"])
+  [("#Given" ,["TERM t_t"]),
+   ("#Find"  ,["normalform n_n"])
   ],
   append_rls "e_rls" e_rls [(*for preds in where_*)], 
-  SOME "Simplify t_", 
+  SOME "Simplify t_t", 
   []));
 
 store_pbt
- (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID
+ (prep_pbt @{theory} "pbl_vereinfache" [] e_pblID
  (["vereinfachen"],
-  [("#Given" ,["TERM t_"]),
-   ("#Find"  ,["normalform n_"])
+  [("#Given" ,["TERM t_t"]),
+   ("#Find"  ,["normalform n_n"])
   ],
   append_rls "e_rls" e_rls [(*for preds in where_*)], 
-  SOME "Vereinfache t_", 
+  SOME "Vereinfache t_t", 
   []));
 
 (** methods **)
 
 store_met
-    (prep_met (theory "Simplify") "met_simp" [] e_metID
+    (prep_met @{theory} "met_tsimp" [] e_metID
 	      (["simplification"],
-	       [("#Given" ,["TERM t_"]),
-		("#Find"  ,["normalform n_"])
+	       [("#Given" ,["TERM t_t"]),
+		("#Find"  ,["normalform n_n"])
 		],
 	       {rew_ord'="tless_true",
 		rls'= e_rls, 
@@ -64,23 +66,23 @@
 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
    make a model which is already in ptree-internal format.*)
 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
-   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
+   val (h,argl) = strip_comb ((term_of o the o (parse (theory "Simplify"))) 
 				  "Simplify (2*a + 3*a)");
    *)
 fun argl2dtss t =
-    [((term_of o the o (parse thy)) "TERM", t),
-     ((term_of o the o (parse thy)) "normalform", 
-      [(term_of o the o (parse thy)) "N"])
+    [((term_of o the o (parse @{theory})) "TERM", t),
+     ((term_of o the o (parse @{theory})) "normalform", 
+      [(term_of o the o (parse @{theory})) "N"])
      ]
   | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
 
 castab := 
 overwritel (!castab, 
-	    [((term_of o the o (parse thy)) "Simplify",  
-	      (("Isac.thy", ["simplification"], ["no_met"]), 
+	    [((term_of o the o (parse @{theory})) "Simplify",  
+	      (("Isac", ["simplification"], ["no_met"]), 
 	       argl2dtss)),
-	     ((term_of o the o (parse thy)) "Vereinfache",  
-	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 
+	     ((term_of o the o (parse @{theory})) "Vereinfache",  
+	      (("Isac", ["vereinfachen"], ["no_met"]), 
 	       argl2dtss))
 	     ]);
 *}