1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Jan 14 18:29:57 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Jan 22 09:33:11 2019 +0100
1.3 @@ -588,7 +588,7 @@
1.4 let
1.5 val formal_arg = TermC.str2term "v_"
1.6 val value = subst_atomic env formal_arg
1.7 - in ["(bdv," ^ Rule.term2str value ^ ")"] : Selem.subs end
1.8 + in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end
1.9 else []
1.10 end
1.11 | "Rulesets" =>
1.12 @@ -600,7 +600,7 @@
1.13 let
1.14 val formal_arg = TermC.str2term "v_"
1.15 val value = subst_atomic env formal_arg
1.16 - in ["(bdv," ^ Rule.term2str value ^ ")"] : Selem.subs end
1.17 + in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end
1.18 else []
1.19 end
1.20 | str => error ("subs_from: uncovered case with " ^ str)
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Jan 14 18:29:57 2019 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Jan 22 09:33:11 2019 +0100
2.3 @@ -291,7 +291,7 @@
2.4 [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);
2.5 B = Take (lastI funs);
2.6 B = ((Substitute cons) @@
2.7 - (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B
2.8 + (Rewrite_Set_Inst [(''bdv'', v)] make_ratpoly_in False)) B
2.9 in B) "
2.10
2.11 \\\------------------------------------------------------------------------------------*)
3.1 --- a/src/Tools/isac/Knowledge/Test.sml Mon Jan 14 18:29:57 2019 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Test.sml Tue Jan 22 09:33:11 2019 +0100
3.3 @@ -1,7 +1,7 @@
3.4 val ttt = (Thm.term_of o the o (parse thy))
3.5 -"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";
3.6 +"(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) e_e";
3.7 val ttt = (Thm.term_of o the o (parse thy))
3.8 -"(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";
3.9 +"(Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) e_e)";
3.10
3.11 val ttt = (Thm.term_of o the o (parse thy))
3.12 "(Rewrite_Set SqRoot_simplify False) e_e ";
3.13 @@ -32,7 +32,7 @@
3.14 val ttt = (Thm.term_of o the o (parse thy))
3.15 "Script Solve_linear (e_e::bool) (v_v::real)= \
3.16 \(let e_e = \
3.17 - \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
3.18 + \ (Repeat ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False)) e_e)\
3.19 \ in [e_e])";
3.20 (*----*)
3.21 val ttt = (Thm.term_of o the o (parse thy))
3.22 @@ -42,7 +42,7 @@
3.23 "Script Solve_linear (e_e::bool) (v_v::real)= \
3.24 \(let e_e = \
3.25 \ (Repeat\
3.26 - \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
3.27 + \ ((%ee_. (Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_)\
3.28 \ e_e)\
3.29 \ e_e)\
3.30 \ in [e_e])";
3.31 @@ -51,7 +51,7 @@
3.32 \(let e_e = \
3.33 \ (Repeat\
3.34 \ ((%ee_.\
3.35 - \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\
3.36 + \ ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_))\
3.37 \ e_e)\
3.38 \ e_e)\
3.39 \ in [e_e])";
3.40 @@ -60,7 +60,7 @@
3.41 \(let e_e = \
3.42 \ (Repeat\
3.43 \ ((%ee_.\
3.44 - \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
3.45 + \ (let e_e = ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_)\
3.46 \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
3.47 \ e_e)\
3.48 \ e_e)\
3.49 @@ -121,22 +121,22 @@
3.50 "Script Solve_linear (e_e::bool) (v_v::real)= \
3.51 \(let e_e = \
3.52 \ ((Repeat\
3.53 - \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
3.54 + \ (((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
3.55 \ (Rewrite_Set SqRoot_simplify False)))) e_e)\
3.56 \ in [e_e])";
3.57 atomty ttt;
3.58
3.59
3.60 val ttt = (Thm.term_of o the o (parse thy))
3.61 -"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";
3.62 +"(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@ yyy";
3.63 atomty ttt;
3.64 val ttt = (Thm.term_of o the o (parse thy))
3.65 - "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
3.66 + "(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
3.67 \ (Rewrite_Set SqRoot_simplify False)";
3.68 atomty ttt;
3.69 val ttt = (Thm.term_of o the o (parse thy))
3.70 "(Repeat\
3.71 - \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
3.72 + \ ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
3.73 \ (Rewrite_Set SqRoot_simplify False))) e_e";
3.74 atomty ttt;
3.75 val ttt = (Thm.term_of o the o (parseold thy))
3.76 @@ -150,7 +150,7 @@
3.77 "Script Solve_linear (e_e::bool) (v_v::real)= \
3.78 \(let e_e =\
3.79 \ Repeat\
3.80 - \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
3.81 + \ (((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
3.82 \ (Rewrite_Set SqRoot_simplify False))) e_\
3.83 \ in [e_::bool])"
3.84 ;
4.1 --- a/src/Tools/isac/library.sml Mon Jan 14 18:29:57 2019 +0100
4.2 +++ b/src/Tools/isac/library.sml Tue Jan 22 09:33:11 2019 +0100
4.3 @@ -287,7 +287,7 @@
4.4 in map strip_thy ((distinct o (con [])) t) end;
4.5
4.6 fun subs2str (subs: string list) = list2str subs;
4.7 -(*> val sss = ["(bdv,x)","(err,#0)"];
4.8 +(*> val sss = ["(''bdv'',x)","(err,#0)"];
4.9 > subs2str sss;
4.10 val it = "[(bdv,x),(err,#0)]" : string*)
4.11 (*\\\------------------------------>>> term ----------------------------------------------///*)
5.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jan 14 18:29:57 2019 +0100
5.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Jan 22 09:33:11 2019 +0100
5.3 @@ -763,7 +763,7 @@
5.4 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.5 (*Rewrite ("all_left","PolyEq.all_left")*)
5.6 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.7 - (*Rewrite_Set_Inst(["(bdv,A)"],"make_ratpoly_in")*)
5.8 + (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
5.9 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.10 (*Rewrite_Set "polyeq_simplify"*)
5.11 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.12 @@ -780,7 +780,7 @@
5.13 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.14 (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
5.15 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.16 - (*Rewrite_Set_Inst(["(bdv,A)"],"d1_polyeq_simplify")*)
5.17 + (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
5.18 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.19 (*Rewrite_Set "polyeq_simplify"*)
5.20 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
5.21 @@ -1390,7 +1390,7 @@
5.22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.23 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
5.24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.25 - (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)
5.26 + (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*)
5.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.30 @@ -1416,7 +1416,7 @@
5.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.32 (*Rewrite ("all_left", "PolyEq.all_left")*)
5.33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.34 - (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
5.35 + (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*)
5.36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.37 (*Rewrite_Set "polyeq_simplify"*)
5.38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.1 --- a/test/Tools/isac/Frontend/use-cases.sml Mon Jan 14 18:29:57 2019 +0100
6.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Tue Jan 22 09:33:11 2019 +0100
6.3 @@ -160,7 +160,7 @@
6.4 (*-------------------------------------------------------------------------*)
6.5
6.6 fetchProposedTactic 1;
6.7 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.8 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
6.9 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.10
6.11 fetchProposedTactic 1;
6.12 @@ -295,7 +295,7 @@
6.13 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.14
6.15 fetchProposedTactic 1;
6.16 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.17 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
6.18 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.19
6.20 fetchProposedTactic 1;
6.21 @@ -621,7 +621,7 @@
6.22 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.23 setNextTactic 1 (Rewrite ("all_left", num_str @{thm all_left}));
6.24 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.25 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
6.26 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
6.27 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.28 (* __________ for "16 + 12 * x = 0"*)
6.29 setNextTactic 1 (Subproblem ("PolyEq",
6.30 @@ -640,7 +640,7 @@
6.31 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.32 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
6.33 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.34 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
6.35 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
6.36 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.37 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
6.38 autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.39 @@ -1110,7 +1110,7 @@
6.40 (*------------------------- end calc-head*)
6.41
6.42 fetchProposedTactic 1;
6.43 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.44 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
6.45 autoCalculate 1 (Step 1);
6.46
6.47 setNextTactic 1 (Rewrite_Set "Test_simplify");
6.48 @@ -1369,7 +1369,7 @@
6.49 val (Form f, _, asms) = pt_extract (pt, p);
6.50
6.51 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
6.52 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
6.53 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.54 ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
6.55 | _ => error "embed fun get_fillform changed 1"
6.56 else error "embed fun get_fillform changed 2";
6.57 @@ -1383,7 +1383,7 @@
6.58
6.59 val (Form f, _, asms) = pt_extract (pt, p);
6.60 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.61 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
6.62 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
6.63 then ()
6.64 else error "embed fun get_fillform changed 2";
6.65
6.66 @@ -1397,7 +1397,7 @@
6.67 val (Form f, _, asms) = pt_extract (pt, p);
6.68 if p = ([1], Res) andalso existpt [2] pt andalso
6.69 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.70 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
6.71 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
6.72 then () else error "embed fun get_fillform changed 3";
6.73
6.74 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
6.75 @@ -1406,7 +1406,7 @@
6.76 val (Form f, _, asms) = pt_extract (pt, p);
6.77 if p = ([2], Res) andalso
6.78 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
6.79 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
6.80 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
6.81 then () else error "inputFillFormula changed 11";
6.82
6.83 autoCalculate 1 CompleteCalc;
7.1 --- a/test/Tools/isac/Interpret/generate.sml Mon Jan 14 18:29:57 2019 +0100
7.2 +++ b/test/Tools/isac/Interpret/generate.sml Tue Jan 22 09:33:11 2019 +0100
7.3 @@ -63,7 +63,7 @@
7.4 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
7.5 val pt = update_branch pt p' TransitiveB;
7.6
7.7 -if get_obj g_tac pt p' = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
7.8 +if get_obj g_tac pt p' = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
7.9 andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
7.10 then () else error "generate_inconsistent_rew changed 3";
7.11
7.12 @@ -77,7 +77,7 @@
7.13 val p = get_pos 1 1;
7.14 val (Form f, _, asms) = pt_extract (pt, p);
7.15 if p = ([2], Res) andalso
7.16 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso
7.17 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
7.18 term2str f =
7.19 "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"
7.20 (*WAS with old findFillpatterns:
8.1 --- a/test/Tools/isac/Interpret/inform.sml Mon Jan 14 18:29:57 2019 +0100
8.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Jan 22 09:33:11 2019 +0100
8.3 @@ -1219,7 +1219,7 @@
8.4 val (Form f, _, asms) = pt_extract (pt, p);
8.5
8.6 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
8.7 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
8.8 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
8.9 ("diff_sum", thm)) =>
8.10 if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
8.11 else error "embed fun get_fillform changed 11"
8.12 @@ -1234,7 +1234,7 @@
8.13
8.14 val (Form f, _, asms) = pt_extract (pt, p);
8.15 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
8.16 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
8.17 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
8.18 ("diff_sum", thm)) =>
8.19 if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
8.20 else error "embed fun get_fillform changed 21"
8.21 @@ -1248,7 +1248,7 @@
8.22 val (Form f, _, asms) = pt_extract (pt, p);
8.23 if p = ([1], Res) andalso existpt [2] pt
8.24 andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
8.25 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
8.26 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
8.27 ("diff_sum", thm)) =>
8.28 if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
8.29 else error "embed fun get_fillform changed 31"
8.30 @@ -1269,7 +1269,7 @@
8.31 val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
8.32 val p' = lev_on p;
8.33 val tac = get_obj g_tac pt p';
8.34 -val Rewrite_Inst ([bbb as "(bdv, x)"], ("diff_sin_chain", ttt)) = tac;
8.35 +val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
8.36 if (term2str o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
8.37 else error "inputFillFormula changed 10";
8.38 val Appl rew = applicable_in pos pt tac;
8.39 @@ -1286,7 +1286,7 @@
8.40 val p = get_pos 1 1;
8.41 val (Form f, _, asms) = pt_extract (pt, p);
8.42 if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
8.43 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
8.44 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
8.45 ("diff_sin_chain", thm)) =>
8.46 if (term2str o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
8.47 else error "inputFillFormula changed 111"
9.1 --- a/test/Tools/isac/Interpret/script.sml Mon Jan 14 18:29:57 2019 +0100
9.2 +++ b/test/Tools/isac/Interpret/script.sml Tue Jan 22 09:33:11 2019 +0100
9.3 @@ -346,7 +346,7 @@
9.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.5 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
9.6 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
9.7 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
9.8 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
9.9
9.10 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
9.11 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.12 @@ -460,7 +460,7 @@
9.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
9.14 val (p'''', pt'''') = (p, pt);
9.15 f2str f = "-1 + x = 0";
9.16 -case snd nxt of Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") => () | _ => error "CHANGED";
9.17 +case snd nxt of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => () | _ => error "CHANGED";
9.18 val (p, p_) = p(* = ([3, 1], Frm)*);
9.19 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
9.20 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
9.21 @@ -481,7 +481,7 @@
9.22 loc_ = [R, L, R, L, R, L, R];
9.23 curry_arg = SOME (str2term "e_e::bool");
9.24 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
9.25 -term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
9.26 +term2str (go loc_ sc) = "Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False";
9.27
9.28 "----------- fun sel_rules ---------------------------------------";
9.29 "----------- fun sel_rules ---------------------------------------";
9.30 @@ -515,7 +515,7 @@
9.31 | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
9.32
9.33 val tacs = sel_rules pt ([3,1],Res);
9.34 - case tacs of [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
9.35 + case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
9.36 | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
9.37
9.38 val tacs = sel_rules pt ([3],Res);
9.39 @@ -659,10 +659,10 @@
9.40 ML> subs;
9.41 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
9.42 > val tt = (Thm.term_of o the o (parse thy))
9.43 - "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
9.44 + "(Rewrite_Inst[(''bdv'',x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
9.45 > atomty tt;
9.46 ML> tracing (term2str tt);
9.47 -(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
9.48 +(Rewrite_Inst [(''bdv'',x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
9.49 #0 + d_d x (x ^^^ #2 + #3 * x)
9.50
9.51 (b)----- laut rep_tac_:
9.52 @@ -672,7 +672,7 @@
9.53
9.54 (*Fehlersuche 1-2Monate vor 4.01:*)
9.55 > val tt = (Thm.term_of o the o (parse thy))
9.56 - "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
9.57 + "Rewrite_Inst[(''bdv'',x)]square_equation_left True(x=#1+#2)";
9.58 > atomty tt;
9.59
9.60 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
10.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Jan 14 18:29:57 2019 +0100
10.2 +++ b/test/Tools/isac/Knowledge/atools.sml Tue Jan 22 09:33:11 2019 +0100
10.3 @@ -169,7 +169,7 @@
10.4
10.5 (* und nach dem Re-engineering der Termorders in den 'rulesets'
10.6 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
10.7 - val bdv= (Thm.term_of o the o (parse thy)) "bdv";
10.8 + val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
10.9 val x = (Thm.term_of o the o (parse thy)) "x";
10.10 val a = (Thm.term_of o the o (parse thy)) "a";
10.11 val b = (Thm.term_of o the o (parse thy)) "b";
11.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Jan 14 18:29:57 2019 +0100
11.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jan 22 09:33:11 2019 +0100
11.3 @@ -141,27 +141,27 @@
11.4 (*val nxt = ("Apply_Method",Apply_Method mI');*)
11.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.6 "--- 1 ---";
11.7 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
11.8 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
11.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.10 "--- 2 ---";
11.11 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
11.12 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
11.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.14 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
11.16 "--- 3 ---";
11.17 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)
11.18 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
11.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.20 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
11.21 "--- 4 ---";
11.22 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_pow","")));*)
11.23 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow","")));*)
11.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.25 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
11.26 "--- 5 ---";
11.27 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)
11.28 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
11.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.30 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
11.31 "--- 6 ---";
11.32 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)
11.33 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var","")));*)
11.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.35 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
11.36 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
11.37 @@ -240,24 +240,24 @@
11.38 \ (Try (Repeat (Rewrite root_conv False))) @@ \
11.39 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
11.40 \ (Repeat \
11.41 - \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \
11.42 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
11.43 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or \
11.44 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or \
11.45 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or \
11.46 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or \
11.47 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or \
11.48 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or \
11.49 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or \
11.50 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or \
11.51 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or \
11.52 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or \
11.53 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or \
11.54 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or \
11.55 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt False)) Or \
11.56 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
11.57 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \
11.58 - \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
11.59 + \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum False)) Or \
11.60 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const False)) Or \
11.61 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod False)) Or \
11.62 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot True )) Or \
11.63 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin False)) Or \
11.64 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain False)) Or \
11.65 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos False)) Or \
11.66 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain False)) Or \
11.67 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow False)) Or \
11.68 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain False)) Or \
11.69 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln False)) Or \
11.70 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain False)) Or \
11.71 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp False)) Or \
11.72 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain False)) Or \
11.73 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt False)) Or \
11.74 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain False)) Or \
11.75 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const False)) Or \
11.76 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var False)) Or \
11.77 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
11.78 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
11.79 \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
12.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Jan 14 18:29:57 2019 +0100
12.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Jan 22 09:33:11 2019 +0100
12.3 @@ -378,14 +378,14 @@
12.4 val str =
12.5 "Script IntegrationScript (f_f::real) (v_v::real) = \
12.6 \ (let t_t = Take (Integral f_f D v_v) \
12.7 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
12.8 +\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))";
12.9 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
12.10 atomty sc;
12.11
12.12 val str =
12.13 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
12.14 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
12.15 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
12.16 +\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)";
12.17 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
12.18 atomty sc;
12.19 show_mets();
12.20 @@ -417,7 +417,7 @@
12.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.22 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
12.23 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
12.24 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
12.25 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
12.26 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.27 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.28 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
13.1 --- a/test/Tools/isac/Knowledge/integrate.thy Mon Jan 14 18:29:57 2019 +0100
13.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Tue Jan 22 09:33:11 2019 +0100
13.3 @@ -16,9 +16,9 @@
13.4 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
13.5 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
13.6 "Script IntegrationScript (f_f::real) (v_v::real) = \
13.7 - \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
13.8 - \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
13.9 - \ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))")]
13.10 + \ (((Rewrite_Set_Inst [(''bdv'',v_v)] integration_rules False) @@ \
13.11 + \ (Rewrite_Set_Inst [(''bdv'',v_v)] add_new_c False) @@ \
13.12 + \ (Rewrite_Set_Inst [(''bdv'',v_v)] simplify_Integral False)) (f_f::real))")]
13.13 \<close>
13.14
13.15 end
14.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Jan 14 18:29:57 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Tue Jan 22 09:33:11 2019 +0100
14.3 @@ -1085,7 +1085,7 @@
14.4
14.5 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
14.6 (*WN.19.3.03 ---v-*)
14.7 -(*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
14.8 +(*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
14.9 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
14.10 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
14.11 term2str t';
14.12 @@ -1098,7 +1098,7 @@
14.13 term2str t';
14.14 "y ^^^ 2 + -2 * x * p = 0";
14.15
14.16 -(*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
14.17 +(*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
14.18 val t = str2term
14.19 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
14.20 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
14.21 @@ -1143,13 +1143,13 @@
14.22 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
14.23 (* steps in rls d2_polyeq_bdv_only_simplify:*)
14.24
14.25 -(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(bdv,x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
14.26 +(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
14.27 t |> term2str; t |> atomty;
14.28 val thm = num_str @{thm d2_prescind1};
14.29 thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
14.30 val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
14.31
14.32 -(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(bdv,x)"],("d2_reduce_equation1",""))
14.33 +(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))
14.34 --> x = 0 | -6 + 5 * x = 0*)
14.35 t' |> term2str; t' |> atomty;
14.36 val thm = num_str @{thm d2_reduce_equation1};
15.1 --- a/test/Tools/isac/Knowledge/rlang.sml Mon Jan 14 18:29:57 2019 +0100
15.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Tue Jan 22 09:33:11 2019 +0100
15.3 @@ -210,7 +210,7 @@
15.4 val v = (Thm.term_of o the o (parse thy)) "x";
15.5 val t = (Thm.term_of o the o (parse thy)) "3 * x / 5";
15.6 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
15.7 - [(bdv, v)] make_ratpoly_in t;
15.8 + [ (bdv, v) ] make_ratpoly_in t;
15.9 if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";
15.10
15.11 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
16.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Jan 14 18:29:57 2019 +0100
16.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Jan 22 09:33:11 2019 +0100
16.3 @@ -480,9 +480,9 @@
16.4 val (p,_,f,nxt,_,pt)=
16.5 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
16.6 "--- 10 ---.";
16.7 -get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt;
16.8 +get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
16.9 val (p,_,f,nxt,_,pt)=
16.10 -me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt;
16.11 +me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt;
16.12 "--- 11 ---";
16.13 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
16.14 val ((p,p_),_,f,nxt,_,pt)=
16.15 @@ -581,7 +581,7 @@
16.16 \Try (Rewrite_Set Test_simplify False)) @@\
16.17 \Try (Rewrite_Set norm_equation False) @@\
16.18 \Try (Rewrite_Set Test_simplify False) @@\
16.19 -\Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False @@\
16.20 +\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False @@\
16.21 \Try (Rewrite_Set Test_simplify False))\
16.22 \e_)";
16.23
16.24 @@ -619,7 +619,7 @@
16.25 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
16.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.27 "--- 12<> ---";
16.28 -val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));
16.29 +val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));
16.30 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.31 "--- 13<> ---";
16.32 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
17.1 --- a/test/Tools/isac/OLDTESTS/script.sml Mon Jan 14 18:29:57 2019 +0100
17.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Tue Jan 22 09:33:11 2019 +0100
17.3 @@ -169,7 +169,7 @@
17.4
17.5 \ e_e = Rewrite_Set norm_equation False e_; \
17.6 \ e_e = Rewrite_Set Test_simplify False e_; \
17.7 - \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
17.8 + \ e_e = Rewrite_Set_Inst [(''bdv'',v_)] isolate_bdv False e_;\
17.9 \ e_e = Rewrite_Set Test_simplify False e_e \
17.10 \ in [e_::bool])";
17.11 val ags = map (Thm.term_of o the o (parse Test.thy))
18.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Jan 14 18:29:57 2019 +0100
18.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Jan 22 09:33:11 2019 +0100
18.3 @@ -279,7 +279,7 @@
18.4 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
18.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.6 "--- 12<> ---.";
18.7 -(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)
18.8 +(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));*)
18.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.10 "--- 13<> ---";
18.11 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
19.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Mon Jan 14 18:29:57 2019 +0100
19.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Tue Jan 22 09:33:11 2019 +0100
19.3 @@ -126,7 +126,7 @@
19.4 (*#######################################################################*)
19.5 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
19.6
19.7 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
19.8 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
19.9 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
19.10
19.11 setNextTactic 1 (Rewrite_Set "Test_simplify");
20.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Mon Jan 14 18:29:57 2019 +0100
20.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Tue Jan 22 09:33:11 2019 +0100
20.3 @@ -143,7 +143,7 @@
20.4 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
20.5
20.6 Rewrite_Inst: subs * thm'' -> tac;
20.7 -val tac = Rewrite_Inst(["(bdv, x)"], ("refl", @{thm refl}));
20.8 +val tac = Rewrite_Inst(["(''bdv'', x)"], ("refl", @{thm refl}));
20.9 if xmlstr 0 (xml_of_tac tac) =
20.10 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^
20.11 ". (SUBSTITUTION)\n" ^
20.12 @@ -196,7 +196,7 @@
20.13 "(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";
20.14
20.15 Rewrite_Set_Inst: subs * rls' -> tac;
20.16 -val tac = Rewrite_Set_Inst(["(bdv, x)"], "simplify");
20.17 +val tac = Rewrite_Set_Inst(["(''bdv'', x)"], "simplify");
20.18 if xmlstr 0 (xml_of_tac tac) =
20.19 "(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^
20.20 ". (SUBSTITUTION)\n" ^