1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -186,7 +186,7 @@
1.4 val rls = Test_simplify;
1.5 val (t,_) = the (rewrite_set_ thy false rls t);
1.6 val rls = isolate_bdv;
1.7 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.8 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.9 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
1.10 val rls = Test_simplify;
1.11 val (t,_) = the (rewrite_set_ thy false rls t);
1.12 @@ -247,7 +247,7 @@
1.13 " _________________ rewrite + cappend _________________ ";
1.14 " _________________ rewrite + cappend _________________ ";
1.15 val thy' = "Test";
1.16 -val ct = TermC.str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.17 +val ct = TermC.parse_test @{context}"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.18 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
1.19 val oris = O_Model.init thy ctl
1.20 ((#ppc o Problem.from_store)
1.21 @@ -290,70 +290,70 @@
1.22 val pos = (lev_on o lev_dn) pos;
1.23 val thm = ("square_equation_left", ""); val ctold = ct;
1.24 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
1.25 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.str2term ct,[])Complete;
1.26 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.parse_test @{context} ct,[])Complete;
1.27 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.28
1.29 val pos = lev_on pos;
1.30 -val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.31 +val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
1.32 val (ct,_) = the (rewrite_set thy' false rls ct);
1.33 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.34 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.35
1.36 val pos = lev_on pos;
1.37 -val rls = ("rearrange_assoc"); val ctold = TermC.str2term ct;
1.38 +val rls = ("rearrange_assoc"); val ctold = TermC.parse_test @{context} ct;
1.39 val (ct,_) = the (rewrite_set thy' false rls ct);
1.40 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.41 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.42
1.43 val pos = lev_on pos;
1.44 -val rls = ("isolate_root"); val ctold = TermC.str2term ct;
1.45 +val rls = ("isolate_root"); val ctold = TermC.parse_test @{context} ct;
1.46 val (ct,_) = the (rewrite_set thy' false rls ct);
1.47 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.48 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.49
1.50 val pos = lev_on pos;
1.51 -val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.52 +val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
1.53 val (ct,_) = the (rewrite_set thy' false rls ct);
1.54 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.55 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.56
1.57 val pos = lev_on pos;
1.58 -val thm = ("square_equation_left", ""); val ctold = TermC.str2term ct;
1.59 +val thm = ("square_equation_left", ""); val ctold = TermC.parse_test @{context} ct;
1.60 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.61 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.62 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.63 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.64
1.65 val pos = lev_up pos;
1.66 -val (pt,_) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
1.67 +val (pt,_) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
1.68
1.69 val pos = lev_on pos;
1.70 -val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.71 +val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
1.72 val (ct,_) = the (rewrite_set thy' false rls ct);
1.73 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.74 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.75
1.76 val pos = lev_on pos;
1.77 -val rls = ("norm_equation"); val ctold = TermC.str2term ct;
1.78 +val rls = ("norm_equation"); val ctold = TermC.parse_test @{context} ct;
1.79 val (ct,_) = the (rewrite_set thy' false rls ct);
1.80 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.81 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.82
1.83 val pos = lev_on pos;
1.84 -val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.85 +val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
1.86 val (ct,_) = the (rewrite_set thy' false rls ct);
1.87 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.88 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.89
1.90 (* --- see comments in interface_ME_ISA/instantiate''
1.91 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
1.92 val (ct,_) = the (rewrite_set thy' false
1.93 ("#isolate_bdv",rlsdat') ct); *)
1.94 val pos = lev_on pos;
1.95 -val rls = ("isolate_bdv"); val ctold = TermC.str2term ct;
1.96 +val rls = ("isolate_bdv"); val ctold = TermC.parse_test @{context} ct;
1.97 val (ct,_) = the (rewrite_set_inst thy' false
1.98 [("bdv", "x")] rls ct);
1.99 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.100 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.101
1.102 val pos = lev_on pos;
1.103 -val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.104 +val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
1.105 val (ct,_) = the (rewrite_set thy' false rls ct);
1.106 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.107 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
1.108
1.109 val pos = lev_up pos;
1.110 -val (pt,pos) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
1.111 +val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
1.112 Ctree.get_assumptions pt ([],Res);
1.113
1.114 writeln (pr_ctree pr_short pt);
1.115 @@ -529,7 +529,7 @@
1.116 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.117
1.118 (*.9.6.03
1.119 - val t = TermC.str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
1.120 + val t = TermC.parse_test @{context} "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
1.121 val SOME (t',asm) = rewrite_set_ thy false rls t;
1.122 UnparseC.term t';
1.123 Rewrite.trace_on:=false; (*true false*)