
diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/Test_Isac.thy
--- a/src/Tools/isac/Test_Isac.thy	Tue Sep 28 13:30:29 2010 +0200
+++ b/src/Tools/isac/Test_Isac.thy	Fri Oct 01 10:23:38 2010 +0200
@@ -9,7 +9,7 @@
         10        20        30        40        50        60        70        80
 *)
 
-theory Test_Isac imports Isac begin
+theory Test_Isac imports "Knowledge/Isac" begin
 
 ML{* writeln "**** run the tests **************************************" *};
 ML {* Toplevel.debug := true; *}
@@ -31,18 +31,21 @@
 cd"smltest/Scripts";
 *)
 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
-
 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
 
-use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*)
+ML {*print_depth 999;*}
+use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)
 (*
 	use"listg.sml";
  	use"scrtools.sml";
  	use"tools.sml";
  	cd "../.."; 
 cd"smltest/ME";
-        use"ctree.sml";
 *)
+use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
+(*      use"ctree.sml";
+*)
+use "../../../test/Tools/isac/Interpret/ptyps.sml";   (*TODO*)
 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
 (*
        	use"calchead.sml"; 
@@ -63,36 +66,45 @@
 *)
 ML{* writeln "**** run tests on math-engine complete ******************" *};
 (*
-cd"smltest/IsacKnowledge";
+cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
         use"atools.sml";
- 	use"complex.sml";
+ 	use"termorder.sml";
+*)
+
+ML {*
+val t = str2term "(x^^^2 * x) is_multUnordered";
+val pat = parse_patt (theory "Isac") "?p is_multUnordered";
+*}
+ML {*
+val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
+Envir.subst_term subst (*pres?*);
+*}
+use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
+(*
+ 	use"rational.sml"
+	use"equation.sml";
+ 	use"root.sml";
+	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
+ 	use"rooteq.sml";
+ 	use"rateq.sml";
+ 	use"rootrateq.sml";
+
+ 	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
+ 			     ? also check others without check 'diff.behav.'*);
+ 	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 
+ 			     for simplification search MG 
+ 		 erls:       98a(1) 104a(1) 104a(2) 68a *);
+	use"wn.sml";
+ 	use"trig.sml";
+ 	use"logexp.sml";
  	use"diff.sml";
- 	use"diffapp.sml";
 *)
 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
 (*
-	use"equation.sml";
-	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
- 	use"logexp.sml";
-*)
-use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
-(*
+	use"eqsystem.sml";
  	use"polyminus.sml";
- 	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
- 			     ? also check others without check 'diff.behav.'*);
- 	use"rateq.sml";
- 	use"rational.sml" (*TODO add_fractions_p throws overflow-exn      WN*);
- 	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 
- 			     for simplification search MG 
- 		 erls:       98a(1) 104a(1) 104a(2) 68a *);
- 	use"root.sml";
- 	use"rooteq.sml";
- 	use"rootrateq.sml";
- 	use"termorder.sml";
- 	use"trig.sml";
  	use"vect.sml";  
-	use"wn.sml";
-	use"eqsystem.sml";
+ 	use"diffapp.sml";
 	use"biegelinie.sml";
 	use"algein.sml";
  	cd "../..";




