1.1 --- a/src/Tools/isac/Build_Isac.thy Sat Feb 24 11:14:56 2018 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sat Feb 24 16:09:24 2018 +0100
1.3 @@ -73,6 +73,40 @@
1.4 ML {*
1.5 *} ML {*
1.6 *}
1.7 +
1.8 +(*==============================================================================================
1.9 + The test below from calculate.sml raises an exception with the cleaned Rewrite.
1.10 + The differences to the working 'fun rewrite' are that significant,
1.11 + that we want to rely on 'hg revert'.
1.12 + For that purpose we save this changeset with a broken 'fun rewrite' and tests not running.
1.13 +*)
1.14 +ML {*
1.15 +open Rewrite
1.16 +*} ML {*
1.17 +*} ML {*
1.18 +(*--------------(2): does divide work in Test_simplify ?: ------*)
1.19 + val thy = @{theory Test};
1.20 + val t = (Thm.term_of o the o (parse thy)) "6 / 2";
1.21 + val rls = Test_simplify;
1.22 +*} ML {*
1.23 + val (t,_) = the (rewrite_set_ thy false rls t);
1.24 +(*val t = Free ("3","Real.real") : term*)
1.25 +*} ML {*
1.26 +
1.27 +(*--------------(3): is_const works ?: -------------------------------------*)
1.28 + val t = (Thm.term_of o the o (parse @{theory})) "2 is_const";
1.29 +*} ML {*
1.30 +*} ML {*
1.31 +*} text {*
1.32 + rewrite_set_ @{theory Test} false tval_rls t;
1.33 +
1.34 +(*exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"):
1.35 + dest_eq
1.36 + 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*)
1.37 +*} ML {*
1.38 +*}
1.39 +(*==============================================================================================*)
1.40 +
1.41 ML {* Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *) *}
1.42 ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.43 ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 11:14:56 2018 +0100
2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 16:09:24 2018 +0100
2.3 @@ -17,10 +17,13 @@
2.4 val rewrite_set_: theory -> bool -> rls -> term -> (term * term list) option
2.5 val rewrite_set_inst_: theory -> bool -> (term * term) list -> rls -> term -> (term * term list) option
2.6 val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> rls -> term list -> term -> (term * term list) option
2.7 +
2.8 +(* doubled intermed., remove !*)
2.9 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option
2.10 +
2.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.12 (* NONE *)
2.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.14 - (* NONE *)
2.15 (* probably shift up ---------------
2.16 exception NO_REWRITE
2.17 exception STOP_REW_SUB
2.18 @@ -37,7 +40,6 @@
2.19 val parse': theory' -> cterm' -> cterm' option
2.20 val rewrite: theory' -> rew_ord' -> rls' -> bool -> thm' -> cterm' -> (string * string) option
2.21 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option
2.22 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option
2.23 val rewrite_inst: theory' -> rew_ord' -> rls' -> bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) option
2.24 val rewrite_set: theory' -> bool -> rls' -> cterm' -> (string * string) option
2.25 val rewrite_set_inst: theory' -> bool -> subs' -> rls' -> cterm' -> (string * string) option
2.26 @@ -75,7 +77,7 @@
2.27 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
2.28 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
2.29 val _ = if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.30 - then tracing (idt "#" (i + 1) ^ " eval asms: " ^ term2str r') else ()
2.31 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ t2str thy r') else ()
2.32 val (t'', p'') = (*conditional rewriting*)
2.33 let
2.34 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
2.35 @@ -83,20 +85,20 @@
2.36 if nofalse
2.37 then
2.38 (if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.39 - then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ terms2str p' ^
2.40 - " stored: " ^ terms2str simpl_p')
2.41 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ ts2str thy p' ^
2.42 + " stored: " ^ ts2str thy simpl_p')
2.43 else();
2.44 (t',simpl_p')) (* uncond.rew. from above*)
2.45 else
2.46 (if ! trace_rewrite andalso i < ! depth
2.47 - then tracing (idt "#" (i + 1) ^ " asms false: " ^ terms2str p')
2.48 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ ts2str thy p')
2.49 else();
2.50 raise STOP_REW_SUB (* don't go into subterms of cond *))
2.51 end
2.52 in
2.53 if perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
2.54 then (if ! trace_rewrite andalso i < ! depth
2.55 - then tracing (idt"#"i ^ " not: \"" ^ term2str t ^ "\" > \"" ^ term2str t' ^ "\"")
2.56 + then tracing (idt"#"i ^ " not: \"" ^ t2str thy t ^ "\" > \"" ^ t2str thy t' ^ "\"")
2.57 else ();
2.58 raise NO_REWRITE)
2.59 else (t'', p'', [], true)
2.60 @@ -134,14 +136,14 @@
2.61 (*asm false .. thm not applied ^^^; continue until False vvv*)
2.62 else chk (indets @ [t] @ a') asms);
2.63 in chk [] asms end
2.64 -and rewrite__set_ _ _ __ Erls t = (* rewrite with a rule set *)
2.65 - error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
2.66 +and rewrite__set_ thy _ __ Erls t = (* rewrite with a rule set *)
2.67 + error ("rewrite__set_ called with 'Erls' for '" ^ t2str thy t ^ "'")
2.68 | rewrite__set_ thy i _ _ (rrls as Rrls _) t = (* rewrite with a 'reverse rule set' *)
2.69 let
2.70 - val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
2.71 - val (t', asm, rew) = app_rev thy (i + 1) rrls t
2.72 + val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ t2str thy t)
2.73 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
2.74 in if rew then SOME (t', distinct asm) else NONE end
2.75 - | rewrite__set_ thy i put_asm bdv rls ct = (* rule set containing Thms or Calculations *)
2.76 + | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Calc, Cal1 *)
2.77 let
2.78 datatype switch = Appl | Noap;
2.79 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with rewtools.sml *)
2.80 @@ -157,7 +159,7 @@
2.81 ((#erls o rep_rls) rls) put_asm thm ct of
2.82 NONE => rew_once ruls asm ct apno thms
2.83 | SOME (ct', asm') =>
2.84 - (trace1 i (" rewrites to: " ^ term2str ct');
2.85 + (trace1 i (" rewrites to: " ^ t2str thy ct');
2.86 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
2.87 | Calc (cc as (op_, _)) =>
2.88 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
2.89 @@ -169,8 +171,8 @@
2.90 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
2.91 ((#erls o rep_rls) rls) put_asm thm' ct;
2.92 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
2.93 - string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
2.94 - val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
2.95 + string_of_thmI thm' ^ "\" " ^ t2str thy ct ^ " = NONE")
2.96 + val _ = trace1 i (" calc. to: " ^ t2str thy ((fst o the) pairopt))
2.97 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
2.98 end
2.99 | Cal1 (cc as (op_, _)) =>
2.100 @@ -183,8 +185,8 @@
2.101 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
2.102 ((#erls o rep_rls) rls) put_asm thm' ct;
2.103 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
2.104 - string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
2.105 - val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
2.106 + string_of_thmI thm' ^ "\" " ^ t2str thy ct ^ " = NONE")
2.107 + val _ = trace1 i (" cal1. to: " ^ t2str thy ((fst o the) pairopt))
2.108 in the pairopt end
2.109 end
2.110 | Rls_ rls' =>
2.111 @@ -193,7 +195,7 @@
2.112 | NONE => rew_once ruls asm ct apno thms)
2.113 | r => raise ERROR ("rew_once not appl. to \"" ^ rule2str r ^ "\"");
2.114 val ruls = (#rules o rep_rls) rls;
2.115 - val _ = trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
2.116 + val _ = trace i (" rls: " ^ id_rls rls ^ " on: " ^ t2str thy ct)
2.117 val (ct', asm') = rew_once ruls [] ct Noap ruls;
2.118 in if ct = ct' then NONE else SOME (ct', distinct asm') end
2.119 and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
3.1 --- a/src/Tools/isac/calcelems.sml Sat Feb 24 11:14:56 2018 +0100
3.2 +++ b/src/Tools/isac/calcelems.sml Sat Feb 24 16:09:24 2018 +0100
3.3 @@ -259,6 +259,8 @@
3.4 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
3.5
3.6 fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
3.7 +fun t2str thy t = term_to_string' (thy2ctxt thy) t;
3.8 +fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
3.9 fun terms2strs ts = map term2str ts;
3.10 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
3.11 val terms2str = strs2str o terms2strs;
3.12 @@ -266,6 +268,7 @@
3.13 val terms2str' = strs2str' o terms2strs;
3.14 (*terms2str' [t1,t2] = "[1 + 2,abc]";*)
3.15
3.16 +
3.17 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
3.18 | termopt2str NONE = "NONE";
3.19
4.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Sat Feb 24 11:14:56 2018 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Sat Feb 24 16:09:24 2018 +0100
4.3 @@ -41,11 +41,11 @@
4.4 ML {*
4.5 val t = (Thm.term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)";
4.6
4.7 -val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.8 -val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.9 -val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_pow t; term2str t;
4.10 -val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_var t; term2str t;
4.11 -val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_const t; term2str t;
4.12 +val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.13 +val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.14 +val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; term2str t;
4.15 +val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; term2str t;
4.16 +val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; term2str t;
4.17 *}
4.18 text {* Please, scoll up the Output-window to check the 5 steps of rewriting !
4.19 You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0".
4.20 @@ -53,7 +53,7 @@
4.21 ISAC has a set of rules called 'make_polynomial', which simplifies the result:
4.22 *}
4.23 ML {*
4.24 -val SOME (t, _) = rewrite_set_ thy true make_polynomial t; term2str t;
4.25 +val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; term2str t;
4.26 trace_rewrite := false;
4.27 *}
4.28
4.29 @@ -79,10 +79,10 @@
4.30 diff_const; let us try: *}
4.31 ML {*
4.32 val t1 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*x*z)";
4.33 -rewrite_inst_ thy ro er true inst diff_const t1;
4.34 +Rewrite.rewrite_inst_ thy ro er true inst diff_const t1;
4.35
4.36 val t2 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*y*z)";
4.37 -rewrite_inst_ thy ro er true inst diff_const t2;
4.38 +Rewrite.rewrite_inst_ thy ro er true inst diff_const t2;
4.39 *}
4.40 text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
4.41 since x occurs in t1 actually; thus the rule following implication '==>' is
4.42 @@ -102,10 +102,10 @@
4.43 text {* Now we want to bring 4*a close to 2*a in order to get 6*a:
4.44 *}
4.45 ML {*
4.46 -val SOME (t, _) = rewrite_ thy ro er true @{thm add.assoc} t0; term2str t;
4.47 -val SOME (t, _) = rewrite_ thy ro er true @{thm add.left_commute} t; term2str t;
4.48 -val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t;
4.49 -val SOME (t, _) = rewrite_ thy ro er true @{thm real_num_collect} t; term2str t;
4.50 +val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.assoc} t0; term2str t;
4.51 +val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.left_commute} t; term2str t;
4.52 +val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; term2str t;
4.53 +val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm real_num_collect} t; term2str t;
4.54 *}
4.55 text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
4.56
4.57 @@ -115,10 +115,10 @@
4.58 as one rule is applicable (that is the way such rulesets work).
4.59 Try to step through the ML-sections without skipping one of them ...
4.60 *}
4.61 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.62 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.63 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.64 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.65 +ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.66 +ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.67 +ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.68 +ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
4.69 text {* ... you can go forever, the ruleset is 'not terminating'.
4.70 The theory of rewriting makes this kind of rulesets terminate by the use of
4.71 'rewrite orders':
4.72 @@ -146,19 +146,19 @@
4.73 ML {*
4.74 (*show_brackets := false; TODO*)
4.75 val t1 = (Thm.term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
4.76 -val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t;
4.77 +val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; term2str t;
4.78 *}
4.79 ML {*
4.80 val t2 = (Thm.term_of o the o (parse thy))
4.81 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))";
4.82 -val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
4.83 +val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; term2str t;
4.84 *}
4.85 text {* The simplifiers are quite busy when finding the above results. you can
4.86 watch them at work by setting the switch 'trace_rewrite:*}
4.87 ML {*
4.88 trace_rewrite := false;
4.89 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
4.90 -val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
4.91 +val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; term2str t;
4.92 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
4.93 trace_rewrite := false;
4.94 *}
4.95 @@ -187,7 +187,7 @@
4.96 ML {*
4.97 val t2 = (Thm.term_of o the o (parse thy))
4.98 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
4.99 -val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t;
4.100 +val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; term2str t;
4.101 *}
4.102 text {* Try your own examples ! *}
4.103
4.104 @@ -227,7 +227,7 @@
4.105 ML {*
4.106 val t = (Thm.term_of o the o (parse thy))
4.107 "(2*a - 5*b) * (2*a + 5*b)";
4.108 -rewrite_set_ thy true rls_p_33 t; term2str t;
4.109 +Rewrite.rewrite_set_ thy true rls_p_33 t; term2str t;
4.110 *}
4.111
4.112 end
5.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sat Feb 24 11:14:56 2018 +0100
5.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sat Feb 24 16:09:24 2018 +0100
5.3 @@ -117,12 +117,13 @@
5.4 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
5.5 ie. cancel does not work properly
5.6 *)
5.7 - val thy = "Test";
5.8 - val op_ = "DIVIDE";
5.9 - val ct = "sqrt (x ^^^ 2 + -3 * x) =\
5.10 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
5.11 - val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
5.12 - writeln ct;
5.13 + val thy = @{theory "Test"};
5.14 + val op_ = the (assoc (calclist, "DIVIDE"));
5.15 + val ct = numbers_to_string @{term
5.16 + "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
5.17 +case calculate_ thy op_ ct of
5.18 + SOME _ => ()
5.19 +| NONE => error "calculate_ test-root-equ changed";
5.20 (*
5.21 sqrt (x ^^^ 2 + -3 * x) =\
5.22 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
5.23 @@ -135,14 +136,6 @@
5.24 val (t,_) = the (rewrite_set_ thy false rls t);
5.25 (*val t = Free ("3","Real.real") : term*)
5.26
5.27 - val thy = "Test";
5.28 - val t = "6 / 2";
5.29 - val rls = "Test_simplify";
5.30 - val (t,_) = the (rewrite_set thy false rls t);
5.31 -(*val t = "3" : string
5.32 - ....... works, thus: which rule in SqRoot_simplify works differently ?*)
5.33 -
5.34 -
5.35 (*--------------(3): is_const works ?: -------------------------------------*)
5.36 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
5.37 atomty t;
5.38 @@ -164,22 +157,6 @@
5.39
5.40 val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
5.41
5.42 - term2str t;
5.43 -"-4 / 2 = (-2)";
5.44 -(*-------------- but ... *)
5.45 - val ct = "x + (-4) / 2";
5.46 -
5.47 -val thy' = "Test"; (* added AK110727 *)
5.48 - val (ct,_) = the (rewrite_set thy' false rls ct);
5.49 -
5.50 -"(-2) + x";
5.51 -(*-------------- while ... *)
5.52 - val ct = "(-4) / 2";
5.53 -
5.54 - val (ct,_) = the (rewrite_set thy' false rls ct);
5.55 -
5.56 -"-2";
5.57 -
5.58 (*--------------(5): reproduce (1) with simpler term: ------------*)
5.59 val thy = "Test";
5.60 val t = "(3+5)/2";
6.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 11:14:56 2018 +0100
6.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 16:09:24 2018 +0100
6.3 @@ -11,8 +11,8 @@
6.4 "table of contents --------------------------------------";
6.5 "--------------------------------------------------------";
6.6 "----------- assemble rewrite ---------------------------";
6.7 -"----------- test rewriting without Isac's thys ---------";
6.8 -"----------- conditional rewriting without Isac's thys --";
6.9 +"----------- test rewriting without Isac session --------";
6.10 +"----------- conditional rewriting without Isac session -";
6.11 "----------- step through 'and rew_sub': ----------------";
6.12 "----------- step through 'fun rewrite_terms_' ---------";
6.13 "----------- rewrite_inst_ bdvs -------------------------";
6.14 @@ -304,7 +304,7 @@
6.15 "===== example which raised the problem =================";
6.16 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
6.17 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
6.18 -val subs = [(str2term "bdv", str2term "x")];
6.19 +val subs = [(@{term "bdv"}, @{term "x"})];
6.20 val rls = norm_Rational_noadd_fractions;
6.21 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
6.22 if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso