1.1 --- a/src/sml/FE-interface/interface.sml Wed Aug 30 12:16:45 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Wed Aug 30 18:50:46 2006 +0200
1.3 @@ -220,7 +220,7 @@
1.4 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.5 (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
1.6 val (cI, p:pos')=(1, ([1],Frm));
1.7 - val (cI, p:pos')=(1, ([1,1,1],Frm));
1.8 + val (cI, p:pos')=(1, ([1,2,1,3],Res));
1.9 *)
1.10 fun getTactic cI (p:pos') =
1.11 (let val ((pt,_),_) = get_calc cI
2.1 --- a/src/sml/ME/ctree.sml Wed Aug 30 12:16:45 2006 +0200
2.2 +++ b/src/sml/ME/ctree.sml Wed Aug 30 18:50:46 2006 +0200
2.3 @@ -514,12 +514,8 @@
2.4 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
2.5 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
2.6
2.7 -(*
2.8 -fun Thm2Rewrite (Thm (thmID,_)) = Rewrite_Set thmID
2.9 - | Thm2Rewrite rule =
2.10 - raise error ("Thm2Rewrite: called with '" ^ rule2str rule ^ "'");
2.11 -*)
2.12 -fun rule2tac (Thm (thmID, thm)) = Rewrite (thmID, string_of_thm thm)
2.13 +fun rule2tac (Thm (thmID, thm)) =
2.14 + Rewrite (thmID, (de_quote o string_of_thm) thm)
2.15 | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
2.16 | rule2tac rule =
2.17 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
3.1 --- a/src/sml/ME/mathengine.sml Wed Aug 30 12:16:45 2006 +0200
3.2 +++ b/src/sml/ME/mathengine.sml Wed Aug 30 18:50:46 2006 +0200
3.3 @@ -399,20 +399,6 @@
3.4 | Some (pI, (pbl, pre)) =>
3.5 (true, pI, hdl, pbl, pre)
3.6 end;
3.7 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.8 -fun tryrefine pI pt (pos as (p,_):pos') =
3.9 - let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
3.10 - in case refine_pbl (assoc_thy "Isac.thy") pI probl of
3.11 - None => (*copy from context_pbl*)
3.12 - let val {ppc,where_,prls,...} = get_pbt pI
3.13 - val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy")
3.14 - probl (ppc,where_,prls) os
3.15 - in (false, pI, hdl, pbl, pre) end
3.16 - | Some (pI, (pbl, pre)) =>
3.17 - (true, pI, hdl, pbl, pre)
3.18 - end;
3.19 -
3.20 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.21
3.22 (* val (pt, (pos as (p,p_):pos')) = (pt, ip);
3.23 *)
4.1 --- a/src/sml/ME/rewtools.sml Wed Aug 30 12:16:45 2006 +0200
4.2 +++ b/src/sml/ME/rewtools.sml Wed Aug 30 18:50:46 2006 +0200
4.3 @@ -86,6 +86,7 @@
4.4 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
4.5 -- replaced below*)
4.6 (* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
4.7 + val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, None, tt);
4.8 *)
4.9 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
4.10 let datatype switch = Appl | Noap
4.11 @@ -151,7 +152,7 @@
4.12 leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
4.13 *)
4.14 in rew_once (!lim_deriv) [] tt Noap rs end;
4.15 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.16 +
4.17
4.18 (*.toggles the marker for 'fun sym_thm'.*)
4.19 fun sym_thmID (thmID : thmID) =
5.1 --- a/src/sml/library.sml Wed Aug 30 12:16:45 2006 +0200
5.2 +++ b/src/sml/library.sml Wed Aug 30 18:50:46 2006 +0200
5.3 @@ -131,7 +131,7 @@
5.4 | scan ss' ("\""::ss) = scan ss' ss
5.5 | scan ss' (s::ss) = scan (ss' @ [s]) ss;
5.6 in (implode o (scan []) o explode) str end;
5.7 -(*> de_esc "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
5.8 +(*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
5.9 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
5.10
5.11
6.1 --- a/src/sml/xmlsrc/datatypes.sml Wed Aug 30 12:16:45 2006 +0200
6.2 +++ b/src/sml/xmlsrc/datatypes.sml Wed Aug 30 18:50:46 2006 +0200
6.3 @@ -554,7 +554,8 @@
6.4 cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac
6.5 'string', _NOT_ 'cterm' ..flaw from RG*)
6.6 indt j ^"</SIMPLETACTIC>\n"):xml
6.7 -
6.8 +(* val (j, Rewrite thm') = (i, tac);
6.9 + *)
6.10 | tac2xml j (Rewrite thm') =
6.11 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
6.12 thm'2xml (j+i) thm'^
7.1 --- a/src/smltest/FE-interface/interface.sml Wed Aug 30 12:16:45 2006 +0200
7.2 +++ b/src/smltest/FE-interface/interface.sml Wed Aug 30 18:50:46 2006 +0200
7.3 @@ -537,8 +537,6 @@
7.4 setContext 1 p "thy_isac_Test-rls-Test_simplify";
7.5 val ((pt,p),_) = get_calc 1; show_pt pt;
7.6
7.7 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
7.8 -
7.9 autoCalculate 1 CompleteCalc;
7.10
7.11
8.1 --- a/src/smltest/IsacKnowledge/rational.sml Wed Aug 30 12:16:45 2006 +0200
8.2 +++ b/src/smltest/IsacKnowledge/rational.sml Wed Aug 30 18:50:46 2006 +0200
8.3 @@ -2045,6 +2045,8 @@
8.4 if length newnds = 12 then ()
8.5 else raise error "rational.sml: interSteps cancel_p rev_rew_p";
8.6
8.7 +getTactic 1 ([1,2,1,9],Res);
8.8 +
8.9
8.10 "-------- investigate rulesets for cancel_p ----------------------";
8.11 "-------- investigate rulesets for cancel_p ----------------------";
9.1 --- a/src/smltest/ME/rewtools.sml Wed Aug 30 12:16:45 2006 +0200
9.2 +++ b/src/smltest/ME/rewtools.sml Wed Aug 30 18:50:46 2006 +0200
9.3 @@ -26,6 +26,7 @@
9.4 "-----------------------------------------------------------------";
9.5
9.6
9.7 +
9.8 "----------- fun collect_isab_thys -------------------------------";
9.9 "----------- fun collect_isab_thys -------------------------------";
9.10 "----------- fun collect_isab_thys -------------------------------";
9.11 @@ -425,3 +426,5 @@
9.12
9.13 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
9.14 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
9.15 +
9.16 +