"sym_thm ... [.]" fixed with "fun string_of_thmI"
1.1 --- a/src/sml/IsacKnowledge/Rational-WN.sml Thu Nov 02 19:19:09 2006 +0100
1.2 +++ b/src/sml/IsacKnowledge/Rational-WN.sml Fri Nov 03 10:51:51 2006 +0100
1.3 @@ -209,7 +209,7 @@
1.4 rls put_asm thm' ct;
1.5 val _ = if pairopt <> None then ()
1.6 else raise error("rewrite_set_, rewrite_ \""^
1.7 - (string_of_thm thm')^"\" \""^
1.8 + (string_of_thmI thm')^"\" \""^
1.9 (Sign.string_of_term (sign_of thy) ct)^"\" = None")
1.10 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.11 val ruls = (#rules o rep_rls) ruless;
1.12 @@ -245,7 +245,7 @@
1.13 rls put_asm thm' ct;
1.14 val _ = if pairopt <> None then ()
1.15 else raise error("rewrite_set_, rewrite_ \""^
1.16 - (string_of_thm thm')^"\" \""^
1.17 + (string_of_thmI thm')^"\" \""^
1.18 (Sign.string_of_term (sign_of thy) ct)^"\" = None")
1.19 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.20 val ruls = (#rules o rep_rls) ruless;
2.1 --- a/src/sml/ME/appl.sml Thu Nov 02 19:19:09 2006 +0100
2.2 +++ b/src/sml/ME/appl.sml Fri Nov 03 10:51:51 2006 +0100
2.3 @@ -539,7 +539,7 @@
2.4 in if msg = "OK" then
2.5 case calculate_ (assoc_thy thy') isa_fn f of
2.6 Some (f', (id, thm)) =>
2.7 - Appl (Calculate' (thy',op_, f, (f', (id, string_of_thm thm))))
2.8 + Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
2.9 | None => Notappl ("'calculate "^op_^"' not applicable")
2.10 else Notappl msg
2.11 end
3.1 --- a/src/sml/ME/calchead.sml Thu Nov 02 19:19:09 2006 +0100
3.2 +++ b/src/sml/ME/calchead.sml Fri Nov 03 10:51:51 2006 +0100
3.3 @@ -2103,6 +2103,7 @@
3.4
3.5 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
3.6 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
3.7 + val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
3.8 *)
3.9 let val ppobj = get_obj I pt p
3.10 val f = if is_pblobj ppobj then pt_model ppobj p_
4.1 --- a/src/sml/ME/ctree.sml Thu Nov 02 19:19:09 2006 +0100
4.2 +++ b/src/sml/ME/ctree.sml Fri Nov 03 10:51:51 2006 +0100
4.3 @@ -515,7 +515,7 @@
4.4 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
4.5
4.6 fun rule2tac (Thm (thmID, thm)) =
4.7 - Rewrite (thmID, (de_quote o string_of_thm) thm)
4.8 + Rewrite (thmID, string_of_thmI thm)
4.9 | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
4.10 | rule2tac rule =
4.11 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
5.1 --- a/src/sml/ME/script.sml Thu Nov 02 19:19:09 2006 +0100
5.2 +++ b/src/sml/ME/script.sml Fri Nov 03 10:51:51 2006 +0100
5.3 @@ -46,13 +46,6 @@
5.4 where 'exp' does not contain a tactic.*)
5.5 val trace_script = ref false;
5.6
5.7 -val string_of_thm' = (implode o tl o drop_last o explode o string_of_thm);
5.8 -(*
5.9 - string_of_thm sym;
5.10 -val it = "\"?s = ?t ==> ?t = ?s\"" : string
5.11 - string_of_thm' sym;
5.12 -val it = "?s = ?t ==> ?t = ?s" : string*)
5.13 -
5.14 type step = (*data for creating a new node in the ptree;
5.15 designed for use:
5.16 fun ass* scrstate steps =
5.17 @@ -65,7 +58,7 @@
5.18 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
5.19 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
5.20
5.21 -fun rule2thm' (Thm (id, thm)) = (id, string_of_thm thm):thm'
5.22 +fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
5.23 | rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));
5.24 fun rule2rls' (Rls_ rls) = id_rls rls
5.25 | rule2rls' r = raise error ("rule2rls': not defined for "^(rule2str r));
5.26 @@ -425,7 +418,7 @@
5.27 (pt, (assoc_thy th), stac);
5.28 *)
5.29 let val tid = (de_esc_underscore o strip_thy) thmID
5.30 - in (Rewrite (tid, (de_quote o string_of_thm o
5.31 + in (Rewrite (tid, (string_of_thmI o
5.32 (assoc_thm' thy)) (tid,"")), Empty_Tac_) end
5.33 (* val (thy,
5.34 mm as(Const ("Script.Rewrite'_Inst",_) $ sub $ Free(thmID,_) $ _ $ f))
5.35 @@ -441,7 +434,7 @@
5.36 val subStr = subst2subs subML
5.37 val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
5.38 in (Rewrite_Inst
5.39 - (subStr, (tid, (de_quote o string_of_thm o
5.40 + (subStr, (tid, (string_of_thmI o
5.41 (assoc_thm' thy)) (tid,""))), Empty_Tac_) end
5.42
5.43 | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f)=
5.44 @@ -1532,6 +1525,7 @@
5.45 (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
5.46 (* val (thy, ptp, E, l, t as Const ("Let",_) $ e $ (Abs (i,T,b)),a, v)=
5.47 (thy, ptp, E, up@[R,D], body, a, v);
5.48 + appy thy ptp E l t a v;
5.49 *)
5.50 ((*writeln("### appy Let$e$Abs: is=");
5.51 writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
5.52 @@ -1618,8 +1612,11 @@
5.53 (case appy thy ptp E (l@[L,R]) e1 a v of
5.54 Appy lme => Appy lme
5.55 | _ => appy thy ptp E (l@[R]) e2 a v)
5.56 +
5.57 (* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)=
5.58 (thy, ptp, E,(up@[R]),e2, a, v);
5.59 + val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)=
5.60 + (thy, ptp, E,(up@[R,D]),body, a, v);
5.61 *)
5.62 | appy thy ptp E l
5.63 (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
5.64 @@ -1628,10 +1625,13 @@
5.65 case appy thy ptp E (l@[L,L,R]) e1 (Some a) v of
5.66 Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (Some a) v
5.67 | ay => ay)
5.68 +
5.69 (* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
5.70 (thy, ptp, E,(up@[R]),e2, a, v);
5.71 val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
5.72 (thy, ptp, E,(l@[R]), e2, a, v);
5.73 + val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
5.74 + (thy, ptp, E,(up@[R,D]),body, a, v);
5.75 *)
5.76 | appy thy ptp E l
5.77 (Const ("Script.Seq",_) $ e1 $ e2) a v =
5.78 @@ -1674,13 +1674,13 @@
5.79 (* val (scr as Script sc, l, t as Const ("Let",_) $ _) =
5.80 (Script sc, up, go up sc);
5.81 nxt_up thy ptp (Script sc) E l ay t a v;
5.82 -val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("Let",_) $ _, a, v)=
5.83 - (thy,ptp,Script sc, E,up,ay, go up sc, a, v);
5.84 +
5.85 + val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("Let",_) $ _, a, v)=
5.86 + (thy,ptp,Script sc, E,up,ay, go up sc, a, v);
5.87 + nxt_up thy ptp scr E l ay t a v;
5.88 *)
5.89 fun nxt_up thy ptp (scr as (Script sc)) E l ay
5.90 (t as Const ("Let",_) $ _) a v = (*comes from let=...*)
5.91 -(* val Const ("Let",_) $ _ = (go up sc);
5.92 - *)
5.93 ((*writeln("### nxt_up1 Let$e: is=");
5.94 writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
5.95 if ay = Napp_
5.96 @@ -1820,9 +1820,9 @@
5.97 (Sign.string_of_term (sign_of (assoc_thy thy)) t))
5.98
5.99 (* val (thy, ptp, (Script sc), E, l, ay, a, v)=
5.100 + (thy, ptp, scr, E, l, Skip_, a, v);
5.101 + val (thy, ptp, (Script sc), E, l, ay, a, v)=
5.102 (thy, ptp, sc, E, l, Skip_, a, v);
5.103 - val (thy, ptp, (Script sc), E, l, ay, a, v)=
5.104 - (thy, ptp, scr, E, l, Skip_, a, v);
5.105 *)
5.106 and nstep_up thy ptp (Script sc) E l ay a v =
5.107 ((*writeln("### nstep_up from: "^(loc_2str l));
5.108 @@ -1864,7 +1864,7 @@
5.109 *)
5.110 | Some (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
5.111 (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
5.112 - (id, string_of_thm' thm), f,(e_term,[(*!?!8.6.03*)])),
5.113 + (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
5.114 Uistate, (e_term, Sundef))) (*next stac*)
5.115
5.116 (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
6.1 --- a/src/sml/Scripts/calculate.sml Thu Nov 02 19:19:09 2006 +0100
6.2 +++ b/src/sml/Scripts/calculate.sml Fri Nov 03 10:51:51 2006 +0100
6.3 @@ -342,9 +342,9 @@
6.4 (read_instantiate subs thm) handle _ => thm)
6.5 | inst_thm' _ calc = calc;
6.6 fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =
6.7 - Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thm thm));
6.8 + Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thmI thm));
6.9 if bdv mem (vars_str o #prop o rep_thm) thm
6.10 - then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thm thm)));
6.11 + then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
6.12 read_instantiate subs thm)
6.13 else (writeln("@@@ inst_thm': not mem.. "^bdv);
6.14 thm)))
7.1 --- a/src/sml/Scripts/rewrite.sml Thu Nov 02 19:19:09 2006 +0100
7.2 +++ b/src/sml/Scripts/rewrite.sml Fri Nov 03 10:51:51 2006 +0100
7.3 @@ -155,8 +155,8 @@
7.4 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
7.5 ((#erls o rep_rls) rls) put_asm thm' ct;
7.6 val _ = if pairopt <> None then ()
7.7 - else raise error("rewrite_set_, rewrite_ "^
7.8 - (string_of_thm thm')^" "^(term2str ct)^" = None")
7.9 + else raise error("rewrite_set_, rewrite_ \""^
7.10 + (string_of_thmI thm')^"\" "^(term2str ct)^" = None")
7.11 val _ = if ! trace_rewrite andalso i < ! depth
7.12 then writeln((idt"="(i+1))^" calc. to: "^
7.13 (term2str ((fst o the) pairopt)))
7.14 @@ -370,7 +370,7 @@
7.15
7.16
7.17 (* outcommented 18.11.xx, xx < 02 -------
7.18 -fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thm thm)
7.19 +fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
7.20 | rul2rul' (Calc op_) = Calc' op_;
7.21 fun rul'2rul thy (Thm'(thmid, ct')) =
7.22 Thm (thmid, mk_thm thy ct')
7.23 @@ -391,7 +391,8 @@
7.24 ------- *)
7.25
7.26 (*.get the theorem associated with the xstring-identifier;
7.27 - if the identifier starts with "sym" then swap lhs = rhs around =;
7.28 + if the identifier starts with "sym_" then swap lhs = rhs around =
7.29 + (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
7.30 identifiers starting with "#" come from Calc and
7.31 get a hand-made theorem (containing numerals only).*)
7.32 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
7.33 @@ -419,8 +420,7 @@
7.34 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
7.35 *** Unknown theorem(s) "real_add_zero_left"
7.36 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
7.37 -
7.38 -uncaught exception ERROR*)
7.39 + uncaught exception ERROR*)
7.40
7.41
7.42 fun parse' (thy:theory') (ct:cterm') =
7.43 @@ -503,7 +503,7 @@
7.44 (parse ((the o assoc')(!theory',thy)))) ct) of
7.45 None => None
7.46 | Some (thmid, thm) =>
7.47 - Some ((thmid, string_of_thm thm):thm');
7.48 + Some ((thmid, string_of_thmI thm):thm');
7.49
7.50 fun calculate (thy':theory') op_ (ct:cterm') =
7.51 let val thy = (the o assoc')(!theory',thy');
7.52 @@ -513,12 +513,12 @@
7.53 None => None
7.54 | Some (ct,(thmID,thm)) =>
7.55 Some (Sign.string_of_term (sign_of thy) ct,
7.56 - (thmID, string_of_thm thm):thm')
7.57 + (thmID, string_of_thmI thm):thm')
7.58 end;
7.59 (*
7.60 fun instantiate'' thy' subs ((thmid,ct'):thm') =
7.61 let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
7.62 - in (thmid_, (string_of_thm o (read_instantiate subs))
7.63 + in (thmid_, (string_of_thmI o (read_instantiate subs))
7.64 ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
7.65
7.66 fun instantiate_rls' thy' subs (rls:rls') =
8.1 --- a/src/sml/calcelems.sml Thu Nov 02 19:19:09 2006 +0100
8.2 +++ b/src/sml/calcelems.sml Fri Nov 03 10:51:51 2006 +0100
8.3 @@ -131,6 +131,18 @@
8.4 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
8.5 (strip_thy thmid1) = (strip_thy thmid2);
8.6
8.7 +(*check for [.] as caused by "fun assoc_thm'"*)
8.8 +fun string_of_thmI thm =
8.9 + let val ct' = (de_quote o string_of_thm) thm
8.10 + val (a, b) = split_nlast (5, explode ct')
8.11 + in case b of
8.12 + [" ", " ","[", ".", "]"] => implode a
8.13 + | _ => ct'
8.14 + end;
8.15 +
8.16 +
8.17 +
8.18 +
8.19 (*.id requested for all, Rls,Seq,Rrls.*)
8.20 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
8.21 | id_rls (Rls {id,...}) = id
8.22 @@ -146,7 +158,7 @@
8.23 | get_rules (Rrls _) = [];
8.24
8.25 fun rule2str Erule = "Erule"
8.26 - | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thm thm)^")"
8.27 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
8.28 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
8.29 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
8.30 fun rule2str' Erule = "Erule"
8.31 @@ -192,7 +204,7 @@
8.32 (1) known by isabelle
8.33 (2) not known, eg. calc_thm, instantiated rls
8.34 the latter have a thmid "#..."
8.35 - and thus outside isa we ALWAYS transport both(thmid,string_of_thm)
8.36 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
8.37 and have a special assoc_thm / assoc_rls in this interface *)
8.38 type theory' = string; (* = domID ^".thy" *)
8.39 type domID = string; (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
9.1 --- a/src/sml/library.sml Thu Nov 02 19:19:09 2006 +0100
9.2 +++ b/src/sml/library.sml Fri Nov 03 10:51:51 2006 +0100
9.3 @@ -86,6 +86,7 @@
9.4
9.5 fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *)
9.6 fun or_ (b1,b2) = b1 orelse b2;
9.7 +
9.8 fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);
9.9 (*> takerest (3, ["normalize","polynomial","univariate","equation"]);
9.10 val it = ["equation"] : string list
9.11 @@ -97,6 +98,17 @@
9.12 val it = ["equation"] : pblID
9.13 > takelast (3, ["normalize","polynomial","univariate","equation"]);
9.14 val it = ["polynomial", "univariate", "equation"]*)
9.15 +fun split_nlast (i, ls) =
9.16 + let val rv = rev ls
9.17 + in (rev (takelast (i - 1, rv)), rev (take (i, rv))) end;
9.18 +
9.19 +fun split_nlast (i, ls) = (take (length ls - i, ls), rev (take (i, rev ls)));
9.20 +(* val (a, b) = split_nlast (3, ["a","b","[",".","]"]);
9.21 +val a = ["a", "b"] : string list
9.22 +val b = ["[", ".", "]"] : string list
9.23 +> val (a, b) = split_nlast (3, [".","]"]);
9.24 +val a = [] : string list
9.25 +val b = [".", "]"] : string list *)
9.26
9.27 (*.analoguous to dropwhile in Pure/libarary.ML.*)
9.28 fun dropwhile P [] = []
9.29 @@ -111,7 +123,6 @@
9.30
9.31
9.32
9.33 -
9.34 fun pair2tri ((a,b),c) = (a,b,c);
9.35 fun fst3 (a,_,_) = a;
9.36 fun snd3 (_,b,_) = b;
10.1 --- a/src/smltest/ME/rewtools.sml Thu Nov 02 19:19:09 2006 +0100
10.2 +++ b/src/smltest/ME/rewtools.sml Fri Nov 03 10:51:51 2006 +0100
10.3 @@ -22,6 +22,7 @@
10.4 "----------- fun guh2theID ---------------------------------------";
10.5 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
10.6 "-----------------------------------------------------------------";
10.7 +"----------- fun string_of_thmI for_[.]_) ------------------------";
10.8 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.9 "-----------------------------------------------------------------";
10.10 "-----------------------------------------------------------------";
10.11 @@ -429,15 +430,50 @@
10.12 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
10.13
10.14
10.15 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.16 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.17 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.18 -"----- these work";
10.19 +"----------- fun string_of_thmI for_[.]_) ------------------------";
10.20 +"----------- fun string_of_thmI for_[.]_) ------------------------";
10.21 +"----------- fun string_of_thmI for_[.]_) ------------------------";
10.22 +"----- these work ?!?";
10.23 val th = sym_thm real_minus_eq_cancel;
10.24 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
10.25 -val th' = mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
10.26 +val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
10.27 +val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
10.28
10.29 -"----- but this generates [.]";
10.30 +"----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
10.31 +val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
10.32 +val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
10.33 + applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
10.34 +"- compose stac as done in | appy (*leaf*) by handle_leaf";
10.35 +val (th, sr, E, a, v, t) =
10.36 + ("Biegelinie.thy",
10.37 + (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
10.38 + [(str2term "q__::bool", str2term "q x = q_0")],
10.39 + Some (str2term "q x = q_0"),
10.40 + str2term "q__::bool",
10.41 + str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
10.42 +val (a', STac stac) = handle_leaf "next " th sr E a v t;
10.43 +term2str stac;
10.44 +"--- but this \"m\" is already corrupted";
10.45 +val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
10.46 +"- because in assoc_thm'...";
10.47 +val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
10.48 +val "s"::"y"::"m"::"_"::id = explode thmid;
10.49 +((num_str o (get_thm thy)) (implode id)) RS sym;
10.50 +((get_thm thy) (implode id)) RS sym;
10.51 +"... this creates [.]";
10.52 +((get_thm thy) (implode id));
10.53 +"... while this has _NO_ [.]";
10.54 +
10.55 +"----- thus we repair the [.] in string_of_thmI...";
10.56 +val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
10.57 +if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
10.58 +else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
10.59 + " = " ^ string_of_thmI thm);
10.60 +
10.61 +
10.62 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.63 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.64 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
10.65 states:=[];
10.66 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
10.67 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
10.68 @@ -449,16 +485,12 @@
10.69 moveActiveRoot 1;
10.70 autoCalculate 1 CompleteCalcHead;
10.71 autoCalculate 1 (Step 1) (*Apply_Method*);
10.72 -"--- this is still ok, when called in next_tac";
10.73 +autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
10.74 +"--- this was corrupted before 'fun string_of_thmI'";
10.75 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
10.76 -val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
10.77 - applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
10.78 -
10.79 -autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
10.80 -"--- but this is already corrupted";
10.81 -val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
10.82 -get_obj g_tac pt p;
10.83 -
10.84 -
10.85 +if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
10.86 + "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
10.87 +else raise error "rewtools.sml: string_of_thmI ?!?";
10.88
10.89 getTactic 1 ([1],Frm);
10.90 +