
diff -r 067d4e3ac358 -r 15775bd26979 src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Thu Sep 09 13:39:30 2010 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Fri Sep 10 10:36:41 2010 +0200
@@ -3,7 +3,7 @@
    (c) due to copyright terms
 *) 
 
-theory Test imports Atools + Rational + Root + Poly + 
+theory Test imports Atools Rational Root Poly begin
  
 consts
 
@@ -29,8 +29,8 @@
 
 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
 
-  "is'_root'_free" :: 'a => bool           ("is'_root'_free _" 10)
-  "contains'_root" :: 'a => bool           ("contains'_root _" 10)
+  "is'_root'_free" :: "'a => bool"           ("is'_root'_free _" 10)
+  "contains'_root" :: "'a => bool"           ("contains'_root _" 10)
 
   Solve'_root'_equation 
              :: "[bool,real,  
@@ -203,9 +203,10 @@
     ]);
 
 (** term order **)
-fun Term_Ord.term_order (_:subst) tu = (term_ordI [] tu = LESS);
-
-(** rule sets GOON **)
+fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
+*}
+ML {*
+(** rule sets **)
 
 val testerls = 
   Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 
@@ -237,7 +238,8 @@
       scr = Script ((term_of o the o (parse thy)) 
       "empty_script")
       }:rls;      
-
+*}
+ML {*
 (*.for evaluation of conditions in rewrite rules.*)
 (*FIXXXXXXME 10.8.02: handle like _simplify*)
 val tval_rls =  
@@ -255,7 +257,7 @@
 	       Thm ("or_true",num_str @{thm or_true}),
 	       Thm ("or_false",num_str @{thm or_false}),
 	       Thm ("and_commute",num_str @{thm and_commute}),
-	       Thm ("or_commute",num_str @{or_commute}),
+	       Thm ("or_commute",num_str @{thm or_commute}),
 
 	       Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
 
@@ -282,7 +284,8 @@
       scr = Script ((term_of o the o (parse thy)) 
       "empty_script")
       }:rls;      
-
+*}
+ML {*
 
 ruleset' := overwritelthy @{theory} (!ruleset',
   [("testerls", prep_rls testerls)
@@ -319,16 +322,17 @@
 val norm_equation =
   Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
       erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
-      rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add)
+      rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
 	       ],
       scr = Script ((term_of o the o (parse thy)) 
       "empty_script")
       }:rls;      
-
+*}
+ML {*
 (** rule sets **)
 
 val STest_simplify =     (*   vv--- not changed to real by parse*)
-  "Script STest_simplify (t_::'z) =                           " ^
+  "Script STest_simplify (t_t::'z) =                           " ^
   "(Repeat" ^
   "    ((Try (Repeat (Rewrite real_diff_minus False))) @@        " ^
   "     (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@  " ^
@@ -372,9 +376,10 @@
   "     (Try (Repeat (Rewrite rmult_0_right False))) @@   " ^
   "     (Try (Repeat (Rewrite radd_0 False))) @@   " ^
   "     (Try (Repeat (Rewrite radd_0_right False)))) " ^
-  " t_)";
+  " t_t)";
 
-
+*}
+ML {*
 (* expects * distributed over + *)
 val Test_simplify =
   Rls{id = "Test_simplify", preconds = [], 
@@ -417,7 +422,7 @@
 	       Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
 	       Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
 	       Thm ("rsqare",num_str @{thm rsqare}),
-	       Thm ("power_1",num_str @{power_1}),
+	       Thm ("power_1",num_str @{thm power_1}),
 	       Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
 	       Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
 
@@ -431,10 +436,8 @@
       scr = Script ((term_of o the o (parse thy)) "empty_script")
 		    (*since 040209 filled by prep_rls: STest_simplify*)
       }:rls;      
-
-
-
-
+*}
+ML {*
 
 (** rule sets **)
 
@@ -462,16 +465,15 @@
 	[Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
 	 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
 	 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
-	 Thm ("mult_square",num_str @{mult_square}),
-	 Thm ("constant_square",num_str @{constant_square}),
-	 Thm ("constant_mult_square",num_str @{constant_mult_square})
+	 Thm ("mult_square",num_str @{thm mult_square}),
+	 Thm ("constant_square",num_str @{thm constant_square}),
+	 Thm ("constant_mult_square",num_str @{thm constant_mult_square})
 	 ],
 	scr = Script ((term_of o the o (parse thy)) 
 			  "empty_script")
 	}:rls;      
-
-
-
+*}
+ML {*
 
 (* association list for calculate_, calculate
    "op +" etc. not usable in scripts *)
@@ -507,6 +509,8 @@
 			 [Calc ("Tools.matches",eval_matches "#matches_")]))
    ]);
 
+*}
+ML {*
 (** problem types **)
 store_pbt
  (prep_pbt thy "pbl_test" [] e_pblID
@@ -537,8 +541,8 @@
  (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
  (["linear","univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_ = 0) e_e) |" ^
-	       "(matches (?a+v_ = 0) e_e) | (matches (?a+?b*v_ = 0) e_e)  "]),
+   ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |" ^
+	       "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)  "]),
    ("#Find"  ,["solutions v_i"])
   ],
   assoc_rls "matches", 
@@ -548,7 +552,7 @@
 store_pbt
  (prep_pbt thy
  (["thy"],
-  [("#Given" ,"boolTestGiven g_"),
+  [("#Given" ,"boolTestGiven g_g"),
    ("#Find"  ,"boolTestFind f_f")
   ],
   []));
@@ -556,7 +560,7 @@
 store_pbt
  (prep_pbt thy
  (["testeq","thy"],
-  [("#Given" ,"boolTestGiven g_"),
+  [("#Given" ,"boolTestGiven g_g"),
    ("#Find"  ,"boolTestFind f_f")
   ],
   []));
@@ -566,7 +570,8 @@
 
  ------ 25.8.01*)
 
-
+*}
+ML {*
 (** methods **)
 store_met
  (prep_met (theory "Diff") "met_test" [] e_metID
@@ -583,6 +588,8 @@
    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
     asm_rls=[],asm_thm=[]},
    "Undef"));*)
+*}
+ML {*
 store_met
  (prep_met thy "met_test_solvelin" [] e_metID
  (["Test","solve_linear"]:metID,
@@ -590,27 +597,26 @@
     ("#Where" ,["matches (?a = ?b) e_e"]),
     ("#Find"  ,["solutions v_i"])
     ],
-   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
-    prls=assoc_rls "matches",
-    calc=[],
-    crls=tval_rls, nrls=Test_simplify},
- "Script Solve_linear (e_e::bool) (v_v::real)=             " ^
- "(let e_e =" ^
- "  Repeat" ^
- "    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
+   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
+    prls = assoc_rls "matches", calc = [], crls = tval_rls,
+    nrls = Test_simplify},
+ "Script Solve_linear (e_e::bool) (v_v::real)=                     " ^
+ "(let e_e =                                                       " ^
+ "  Repeat                                                         " ^
+ "    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@  " ^
  "      (Rewrite_Set Test_simplify False))) e_e" ^
- " in [e_::bool])"
+ " in [e_e::bool])"
  )
 (*, prep_met thy (*test for equations*)
  (["Test","testeq"]:metID,
-  [("#Given" ,["boolTestGiven g_"]),
+  [("#Given" ,["boolTestGiven g_g"]),
    ("#Find"  ,["boolTestFind f_f"])
     ],
   {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
    asm_thm=[("square_equation_left","")]},
- "Script Testeq (eq_::bool) =                                         " ^
+ "Script Testeq (e_q::bool) =                                         " ^
    "Repeat                                                            " ^
-   " (let e_e = Try (Repeat (Rewrite rroot_square_inv False eq_));      " ^
+   " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q));      " ^
    "      e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
    "      e_e = Try (Repeat (Rewrite rmult_0 False e_e))                " ^
    "   in e_e) Until (is_root_free e_e)" (*deleted*)
@@ -618,8 +624,8 @@
 , ---------27.4.02*)
 );
 
-
-
+*}
+ML {*
 
 ruleset' := overwritelthy @{theory} (!ruleset',
   [("norm_equation", prep_rls norm_equation),
@@ -764,7 +770,8 @@
 fun rational t div_op bdVar = 
     is_denom bdVar div_op t andalso bin_ops_only t;
 
-
+*}
+ML {*
 
 (** problem types **)
 
@@ -772,8 +779,8 @@
  (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
  (["plain_square","univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
-	       "(matches (     ?b*v_ ^^^2 = 0) e_e) |" ^
+   ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
+	       "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (        v_v ^^^2 = 0) e_e)"]),
    ("#Find"  ,["solutions v_i"])
@@ -781,13 +788,13 @@
   assoc_rls "matches", 
   SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
 (*
- val e_e = (term_of o the o (parse thy)) "e_::bool";
+ val e_e = (term_of o the o (parse thy)) "e_e::bool";
  val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
  val env = [(e_,ve)];
 
  val pre = (term_of o the o (parse thy))
-	      "(matches (a + b*v_ ^^^2 = 0, e_e::bool)) |" ^
-	      "(matches (    b*v_ ^^^2 = 0, e_e::bool)) |" ^
+	      "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
+	      "(matches (    b*v_v ^^^2 = 0, e_e::bool)) |" ^
 	      "(matches (a +   v_v ^^^2 = 0, e_e::bool)) |" ^
 	      "(matches (      v_v ^^^2 = 0, e_e::bool))";
  val prei = subst_atomic env pre;
@@ -803,10 +810,12 @@
 
 *)
 
+*}
+ML {*
 store_pbt
  (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
  (["polynomial","univariate","equation","test"],
-  [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
+  [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
    ("#Where" ,["False"]),
    ("#Find"  ,["solutions v_i"]) 
   ],
@@ -815,27 +824,29 @@
 store_pbt
  (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
  (["degree_two","polynomial","univariate","equation","test"],
-  [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
+  [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
    ("#Find"  ,["solutions v_i"]) 
   ],
-  e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
+  e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 
 store_pbt
  (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
  (["pq_formula","degree_two","polynomial","univariate","equation","test"],
-  [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
+  [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
    ("#Find"  ,["solutions v_i"]) 
   ],
-  e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
+  e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 
 store_pbt
  (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
  (["abc_formula","degree_two","polynomial","univariate","equation","test"],
-  [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_v"]),
+  [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
    ("#Find"  ,["solutions v_i"]) 
   ],
-  e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_v)", []));
+  e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
 
+*}
+ML {*
 store_pbt
  (prep_pbt thy "pbl_test_uni_root" [] e_pblID
  (["squareroot","univariate","equation","test"],
@@ -868,6 +879,8 @@
 (*
 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
   *)
+*}
+ML {*
 
 
 store_met
@@ -900,9 +913,11 @@
  "    (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e" ^
- " in [e_::bool])"
+ " in [e_e::bool])"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy  "met_test_sqrt2" [] e_metID
 (*root-equation ... for test-*.sml until 8.01*)
@@ -930,11 +945,13 @@
  "    (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e;" ^
- "  (L_::bool list) = Tac subproblem_equation_dummy;          " ^
+ "  (L_L::bool list) = Tac subproblem_equation_dummy;          " ^
  "  L_L = Tac solve_equation_dummy                             " ^
  "  in Check_elementwise L_L {(v_v::real). Assumptions})"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_squ_sub" [] e_metID
 (*tests subproblem fixed linear*)
@@ -944,14 +961,18 @@
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
     crls=tval_rls, nrls=Test_simplify},
-  "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
-   " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@              " ^
-   "            (Try (Rewrite_Set Test_simplify False))) e_e;              " ^
-   "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
-   "                    [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
+  "Script Solve_root_equation (e_e::bool) (v_v::real) =                " ^
+   " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@            " ^
+   "            (Try (Rewrite_Set Test_simplify False))) e_e;          " ^
+   "(L_L::bool list) = (SubProblem (Test',                             " ^
+   "                                [linear,univariate,equation,test], " ^
+   "                                [Test,solve_linear])" ^
+   "                               [BOOL e_e, REAL v_v])" ^
    "in Check_elementwise L_L {(v_v::real). Assumptions})"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_squ_sub2" [] e_metID
  (*tests subproblem fixed degree 2*)
@@ -965,11 +986,13 @@
 	    ("square_equation_right","")]*)},
    "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    " (let e_e = Try (Rewrite_Set norm_equation False) e_e;              " ^
-   "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
-   "                    [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^
+   "(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
+   "                    [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
    "in Check_elementwise L_L {(v_v::real). Assumptions})"
    )); 
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_squ_nonterm" [] e_metID
  (*root-equation: see foils..., but notTerminating*)
@@ -995,12 +1018,14 @@
  "    (Try (Rewrite_Set norm_equation False)) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e;" ^
- "  (L_::bool list) =                                        " ^
- "    (SubProblem (Test_,[linear,univariate,equation,test]," ^
- "                 [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
+ "  (L_L::bool list) =                                        " ^
+ "    (SubProblem (Test',[linear,univariate,equation,test]," ^
+ "                 [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
  "in Check_elementwise L_L {(v_v::real). Assumptions})"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy  "met_test_eq1" [] e_metID
 (*root-equation1:*)
@@ -1026,11 +1051,13 @@
  "    (Try (Rewrite_Set norm_equation False)) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e;" ^
- "  (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
- "                    [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
+ "  (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
+ "                    [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
  "  in Check_elementwise L_L {(v_v::real). Assumptions})"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_squ2" [] e_metID
  (*root-equation2*)
@@ -1057,11 +1084,13 @@
  "    (Try (Rewrite_Set norm_equation False)) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e;" ^
- "  (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
- "                    [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^
+ "  (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
+ "                    [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
  "  in Check_elementwise L_L {(v_v::real). Assumptions})"
   ));
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_squeq" [] e_metID
  (*root-equation*)
@@ -1088,18 +1117,20 @@
  "    (Try (Rewrite_Set norm_equation False)) @@" ^
  "    (Try (Rewrite_Set Test_simplify False)))" ^
  "   e_e;" ^
- "  (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
- "                    [no_met]) [BOOL e_e, REAL v_])" ^
+ "  (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
+ "                    [no_met]) [BOOL e_e, REAL v_v])" ^
  "  in Check_elementwise L_L {(v_v::real). Assumptions})"
   ) ); (*#######*)
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_eq_plain" [] e_metID
  (*solve_plain_square*)
  (["Test","solve_plain_square"]:metID,
    [("#Given",["equality e_e","solveFor v_v"]),
-   ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
-	       "(matches (     ?b*v_ ^^^2 = 0) e_e) |" ^
+   ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
+	       "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (        v_v ^^^2 = 0) e_e)"]), 
    ("#Find"  ,["solutions v_i"]) 
@@ -1117,6 +1148,8 @@
    "  in ((Or_to_List e_e)::bool list))"
  ));
 
+*}
+ML {*
 store_met
  (prep_met thy "met_test_norm_univ" [] e_metID
  (["Test","norm_univar_equation"]:metID,
@@ -1130,13 +1163,15 @@
   "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
    " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@   " ^
    "            (Try (Rewrite_Set Test_simplify False))) e_e   " ^
-   "  in (SubProblem (Test_,[univariate,equation,test],         " ^
-   "                    [no_met]) [BOOL e_e, REAL v_]))"
+   "  in (SubProblem (Test',[univariate,equation,test],         " ^
+   "                    [no_met]) [BOOL e_e, REAL v_v]))"
  ));
 
 
 
 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)  
+*}
+ML {*
 
 (*8.4.03  aus Poly.ML--------------------------------vvv---
   make_polynomial  ---> make_poly
@@ -1171,18 +1206,18 @@
   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
   | size_of_term' _ = 1;
 
-fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
-      (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
-  | Term_Ord.term_ord' pr thy (t, u) =
+fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
+      (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
+  | term_ord' pr thy (t, u) =
       (if pr then 
 	 let
 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
 	   val _=writeln("t= f@ts= " ^ "" ^
 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^
-	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]""");
+	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\"");
 	   val _=writeln("u= g@us= " ^ "" ^
 	      ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^
-	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]""");
+	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
 	   val _=writeln("size_of_term(t,u)= ("^
 	      (string_of_int(size_of_term' t)) ^ ", " ^
 	      (string_of_int(size_of_term' u)) ^ ")");
@@ -1209,6 +1244,8 @@
     (term_ord' pr thy(***) tu = LESS );
 
 end;(*local*)
+*}
+ML {*
 
 rew_ord' := overwritel (!rew_ord',
 [("termlessI", termlessI),
@@ -1217,7 +1254,7 @@
 
 (*WN060510 this was a preparation for prep_rls ...
 val scr_make_polytest = 
-"Script Expand_binomtest t_ =" ^
+"Script Expand_binomtest t_t =" ^
 "(Repeat                       " ^
 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
 
@@ -1251,7 +1288,7 @@
 " (Try (Repeat (Calculate PLUS  ))) @@ " ^
 " (Try (Repeat (Calculate TIMES ))) @@ " ^
 " (Try (Repeat (Calculate POWER)))) " ^  
-" t_)";
+" t_t)";
 -----------------------------------------------------*)
 
 val make_polytest =
@@ -1321,10 +1358,12 @@
 	       ],
       scr = EmptyScr(*Script ((term_of o the o (parse thy)) 
       scr_make_polytest)*)
-      }:rls;      
-(*WN060510 this was done before 'fun prep_rls' ...
+      }:rls; 
+*}
+ML {*     
+(*WN060510 this was done before 'fun prep_rls' ...------------------------
 val scr_expand_binomtest =
-"Script Expand_binomtest t_ =" ^
+"Script Expand_binomtest t_t =" ^
 "(Repeat                       " ^
 "((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^
 " (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^
@@ -1355,8 +1394,8 @@
 " (Try (Repeat (Calculate PLUS  ))) @@ " ^
 " (Try (Repeat (Calculate TIMES ))) @@ " ^
 " (Try (Repeat (Calculate POWER)))) " ^  
-" t_)";
-------------------------------------------------------*)
+" t_t)";
+--------------------------------------------------------------------------*)
 
 val expand_binomtest =
   Rls{id = "expand_binomtest", preconds = [], 
@@ -1366,85 +1405,90 @@
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
-      rules = [Thm ("real_plus_binom_pow2"  ,num_str @{thm real_plus_binom_pow2}),     
+      rules = 
+      [Thm ("real_plus_binom_pow2"  ,num_str @{thm real_plus_binom_pow2}),     
 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
-	       Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),    
+       Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),    
 	      (*"(a + b)*(a + b) = ...*)
-	       Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),   
-	       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
-	       Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),   
-	       (*"(a - b)*(a - b) = ...*)
-	       Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),   
-		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
-	       Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),   
-		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
-	       (*RL 020915*)
-	       Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), 
-		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
-               Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), 
-		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
-               Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), 
-		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
-               Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), 
-		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
-	       Thm ("realpow_multI",num_str @{thm realpow_multI}),                
-		(*(a*b)^^^n = a^^^n * b^^^n*)
-	       Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
-	        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
-	       Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
-	        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
+       Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),   
+       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
+       Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),   
+       (*"(a - b)*(a - b) = ...*)
+       Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),   
+        (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
+       Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),   
+        (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
+       (*RL 020915*)
+       Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), 
+        (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
+       Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), 
+        (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
+       Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), 
+        (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
+       Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), 
+        (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
+       Thm ("realpow_multI",num_str @{thm realpow_multI}),                
+        (*(a*b)^^^n = a^^^n * b^^^n*)
+       Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
+        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
+       Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
+        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
 
 
-             (*  Thm ("left_distrib" ,num_str @{thm left_distrib}}),	
-		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
-	       Thm ("right_distrib",num_str @{thm right_distrib}),	
-	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
-	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),	
-	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
-	       Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),	
-	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
-	       *)
-	       
-	       Thm ("mult_1_left",num_str @{thm mult_1_left}}),              (*"1 * z = z"*)
-	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}}),              (*"0 * z = 0"*)
-	       Thm ("add_0_left",num_str @{thm add_0_left}}),(*"0 + z = z"*)
+     (*  Thm ("left_distrib" ,num_str @{thm left_distrib}),	
+	 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
+	Thm ("right_distrib",num_str @{thm right_distrib}),	
+	(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
+	Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),	
+	(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
+	Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),	
+	(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
+	*)
+	
+	Thm ("mult_1_left",num_str @{thm mult_1_left}),              
+         (*"1 * z = z"*)
+	Thm ("mult_zero_left",num_str @{thm mult_zero_left}),              
+         (*"0 * z = 0"*)
+	Thm ("add_0_left",num_str @{thm add_0_left}),
+         (*"0 + z = z"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
-	       Calc ("op *", eval_binop "#mult_"),
-	       Calc ("Atools.pow", eval_binop "#power_"),
-               (*	       
-	        Thm ("real_mult_commute",num_str @{thm real_mult_commute}),		(*AC-rewriting*)
-	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),	(**)
-	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),			(**)
-	       Thm ("add_commute",num_str @{thm add_commute}),		(**)
-	       Thm ("add_left_commute",num_str @{thm add_left_commute}),	(**)
-	       Thm ("add_assoc",num_str @{thm add_assoc}),	                (**)
-	       *)
-	       
-	       Thm ("sym_realpow_twoI",
-                     num_str (@{thm realpow_twoI} RS @{thm sym})),
-	       (*"r1 * r1 = r1 ^^^ 2"*)
-	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			
-	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
-	       (*Thm ("sym_real_mult_2",
-                       num_str (@{thm real_mult_2} RS @{thm sym})),
-	       (*"z1 + z1 = 2 * z1"*)*)
-	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		
-	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
+	Calc ("op +", eval_binop "#add_"), 
+	Calc ("op *", eval_binop "#mult_"),
+	Calc ("Atools.pow", eval_binop "#power_"),
+        (*	       
+	 Thm ("real_mult_commute",num_str @{thm real_mult_commute}),		
+        (*AC-rewriting*)
+	Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
+	Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
+	Thm ("add_commute",num_str @{thm add_commute}),	
+	Thm ("add_left_commute",num_str @{thm add_left_commute}),
+	Thm ("add_assoc",num_str @{thm add_assoc}),
+	*)
+	
+	Thm ("sym_realpow_twoI",
+              num_str (@{thm realpow_twoI} RS @{thm sym})),
+	(*"r1 * r1 = r1 ^^^ 2"*)
+	Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			
+	(*"r * r ^^^ n = r ^^^ (n + 1)"*)
+	(*Thm ("sym_real_mult_2",
+                num_str (@{thm real_mult_2} RS @{thm sym})),
+	(*"z1 + z1 = 2 * z1"*)*)
+	Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		
+	(*"z1 + (z1 + k) = 2 * z1 + k"*)
 
-	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 
-	       (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
-	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),	
-	       (*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
-	       Thm ("real_one_collect",num_str @{thm real_one_collect}),		
-	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
-	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
-	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
+	Thm ("real_num_collect",num_str @{thm real_num_collect}), 
+	(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
+	Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),	
+	(*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
+	Thm ("real_one_collect",num_str @{thm real_one_collect}),		
+	(*"m is_const ==> n + m * n = (1 + m) * n"*)
+	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
+	(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
-	       Calc ("op *", eval_binop "#mult_"),
-	       Calc ("Atools.pow", eval_binop "#power_")
-	       ],
+	Calc ("op +", eval_binop "#add_"), 
+	Calc ("op *", eval_binop "#mult_"),
+	Calc ("Atools.pow", eval_binop "#power_")
+	],
       scr = EmptyScr
 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
       }:rls;      




