Isabelle2015->17: completed "normalise" cf. fb6f5ef2c647
1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Feb 13 16:17:59 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Feb 14 06:06:27 2018 +0100
1.3 @@ -48,7 +48,7 @@
1.4 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]
1.5 ==>(a * b = c) = (b = c / a)"
1.6 axiomatization where (*..if replaced by "and" we get an error in
1.7 - --- rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*)
1.8 + --- rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*)
1.9 order_system_NxN: "[a,b] = [b,a]"
1.10 (*requires rew_ord for termination, eg. ord_simplify_Integral;
1.11 works for lists of any length, interestingly !?!*)
1.12 @@ -498,7 +498,7 @@
1.13
1.14 ML {*
1.15 (*this is for NTH only*)
1.16 -val srls = Rls {id="srls_normalize_4x4",
1.17 +val srls = Rls {id="srls_normalise_4x4",
1.18 preconds = [],
1.19 rew_ord = ("termlessI",termlessI),
1.20 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.21 @@ -582,7 +582,7 @@
1.22 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.23 ("#Find" ,["solution ss'''"])],
1.24 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.25 - srls = append_rls "srls_normalize_2x2" e_rls
1.26 + srls = append_rls "srls_normalise_2x2" e_rls
1.27 [Thm ("hd_thm",num_str @{thm hd_thm}),
1.28 Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.29 Thm ("tl_Nil",num_str @{thm tl_Nil})],
1.30 @@ -603,7 +603,7 @@
1.31 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.32 ("#Find" ,["solution ss'''"])],
1.33 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.34 - srls = append_rls "srls_normalize_4x4" srls
1.35 + srls = append_rls "srls_normalise_4x4" srls
1.36 [Thm ("hd_thm",num_str @{thm hd_thm}),
1.37 Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.38 Thm ("tl_Nil",num_str @{thm tl_Nil})],
2.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Feb 13 16:17:59 2018 +0100
2.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Feb 14 06:06:27 2018 +0100
2.3 @@ -16,7 +16,7 @@
2.4 ("((Script Solve'_lineq'_equation (_ _ =))// (_))" 9)
2.5
2.6 axiomatization where
2.7 -(*-- normalize --*)
2.8 +(*-- normalise --*)
2.9 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
2.10 all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
2.11 makex1_x: "a^^^1 = a" and
3.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Feb 13 16:17:59 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Feb 14 06:06:27 2018 +0100
3.3 @@ -122,7 +122,7 @@
3.4 plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) and
3.5 minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) and
3.6
3.7 -(*-- normalize --*)
3.8 +(*-- normalise --*)
3.9 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
3.10 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
3.11 makex1_x: "a^^^1 = a" and
3.12 @@ -928,14 +928,14 @@
3.13 "((lhs e_e) has_degree_in v_v) = 4"]),
3.14 ("#Find", ["solutions v_v'i'"])],
3.15 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
3.16 - (*--- normalize ---*)
3.17 + (*--- normalise ---*)
3.18 (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
3.19 (["normalise","polynomial","univariate","equation"],
3.20 [("#Given", ["equality e_e","solveFor v_v"]),
3.21 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
3.22 "(Not(((lhs e_e) is_poly_in v_v)))"]),
3.23 ("#Find", ["solutions v_v'i'"])],
3.24 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])),
3.25 + PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalise_poly"]])),
3.26 (*-------------------------expanded-----------------------*)
3.27 (Specify.prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
3.28 (["expanded","univariate","equation"],
3.29 @@ -974,7 +974,7 @@
3.30 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
3.31 "empty_script"),
3.32 Specify.prep_met thy "met_polyeq_norm" [] e_metID
3.33 - (["PolyEq","normalize_poly"],
3.34 + (["PolyEq","normalise_poly"],
3.35 [("#Given" ,["equality e_e","solveFor v_v"]),
3.36 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),
3.37 ("#Find" ,["solutions v_v'i'"])],
3.38 @@ -1118,7 +1118,7 @@
3.39 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
3.40 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
3.41 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
3.42 - (*.solves all expanded (ie. normalized) terms of degree 2.*)
3.43 + (*.solves all expanded (ie. normalised) terms of degree 2.*)
3.44 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
3.45 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
3.46 Specify.prep_met thy "met_polyeq_complsq" [] e_metID
4.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Feb 13 16:17:59 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Feb 14 06:06:27 2018 +0100
4.3 @@ -4,7 +4,7 @@
4.4 Use is subject to license terms.
4.5
4.6 depends on Poly (and not on Atools), because
4.7 - fractions with _normalized_ polynomials are canceled, added, etc.
4.8 + fractions with _normalised_ polynomials are canceled, added, etc.
4.9 *)
4.10
4.11 theory Rational
5.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Feb 13 16:17:59 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Feb 14 06:06:27 2018 +0100
5.3 @@ -45,7 +45,7 @@
5.4
5.5 axiomatization where
5.6
5.7 -(* normalize *)
5.8 +(* normalise *)
5.9 makex1_x: "a^^^1 = a" and
5.10 real_assoc_1: "a+(b+c) = a+b+c" and
5.11 real_assoc_2: "a*(b*c) = a*b*c" and
5.12 @@ -73,7 +73,7 @@
5.13 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and
5.14 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
5.15 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and
5.16 - (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
5.17 + (* small hack: thm 3,5,6 are not needed if rootnormalise is well done*)
5.18 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
5.19 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and
5.20 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
5.21 @@ -102,7 +102,7 @@
5.22 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and
5.23 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
5.24 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and
5.25 - (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
5.26 + (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
5.27 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
5.28 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" and
5.29 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
5.30 @@ -115,7 +115,7 @@
5.31 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and
5.32 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
5.33 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and
5.34 - (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
5.35 + (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
5.36 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
5.37 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" and
5.38 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
5.39 @@ -156,7 +156,7 @@
5.40 end;
5.41
5.42 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
5.43 -and the subterm ist connected with + or * --> is normalized*)
5.44 +and the subterm ist connected with + or * --> is normalised*)
5.45 fun is_normSqrtTerm_in t v =
5.46 let
5.47 fun coeff_in c v = member op = (vars c) v;
5.48 @@ -501,7 +501,7 @@
5.49 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
5.50 ("#Find" ,["solutions v_v'i'"])],
5.51 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),
5.52 - (* ---------normalize----------- *)
5.53 + (* ---------normalise----------- *)
5.54 (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
5.55 (["normalise","root'","univariate","equation"],
5.56 [("#Given" ,["equality e_e","solveFor v_v"]),
5.57 @@ -520,7 +520,7 @@
5.58 (["RootEq"], [],
5.59 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
5.60 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"),
5.61 - (*-- normalize 20.10.02 --*)
5.62 + (*-- normalise 20.10.02 --*)
5.63 Specify.prep_met thy "met_rooteq_norm" [] e_metID
5.64 (["RootEq","norm_sq_root_equation"],
5.65 [("#Given" ,["equality e_e","solveFor v_v"]),
5.66 @@ -538,9 +538,7 @@
5.67 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
5.68 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
5.69 " in ((SubProblem (RootEq',[univariate,equation], " ^
5.70 - " [no_met]) [BOOL e_e, REAL v_v])))")
5.71 -(*----- broke at Isabelle2015 \<longrightarrow> Isabelle2017, reason unknown -----
5.72 -,
5.73 + " [no_met]) [BOOL e_e, REAL v_v])))"),
5.74 Specify.prep_met thy "met_rooteq_sq" [] e_metID
5.75 (["RootEq","solve_sq_root_equation"],
5.76 [("#Given" ,["equality e_e", "solveFor v_v"]),
5.77 @@ -560,7 +558,7 @@
5.78 " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
5.79 " (L_L::bool list) = " ^
5.80 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
5.81 - " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
5.82 + " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
5.83 " [no_met]) [BOOL e_e, REAL v_v]) " ^
5.84 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
5.85 " [BOOL e_e, REAL v_v])) " ^
5.86 @@ -581,7 +579,7 @@
5.87 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
5.88 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
5.89 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
5.90 - " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
5.91 + " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
5.92 " [no_met]) [BOOL e_e, REAL v_v]) " ^
5.93 " else ((SubProblem (RootEq',[univariate,equation], " ^
5.94 " [no_met]) [BOOL e_e, REAL v_v])))"),
5.95 @@ -601,13 +599,10 @@
5.96 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
5.97 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
5.98 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
5.99 - " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
5.100 + " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
5.101 " [no_met]) [BOOL e_e, REAL v_v]) " ^
5.102 " else ((SubProblem (RootEq',[univariate,equation], " ^
5.103 - " [no_met]) [BOOL e_e, REAL v_v])))")
5.104 ------ broke at Isabelle2015 \<longrightarrow> Isabelle2017, reason unknown -------*)
5.105 -]
5.106 -*}
5.107 + " [no_met]) [BOOL e_e, REAL v_v])))")] *}
5.108
5.109 setup {* KEStore_Elems.add_calcs
5.110 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),
6.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Feb 13 16:17:59 2018 +0100
6.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Feb 14 06:06:27 2018 +0100
6.3 @@ -110,7 +110,7 @@
6.4 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
6.5 str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
6.6 (* term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalise"]);
6.7 -val it = "Problem (Isac, [normalize, univariate, equations])" : string
6.8 +val it = "Problem (Isac, [normalise, univariate, equations])" : string
6.9 *)
6.10 val i = indentation;
6.11
7.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Feb 13 16:17:59 2018 +0100
7.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Feb 14 06:06:27 2018 +0100
7.3 @@ -759,9 +759,9 @@
7.4 (*Specify_Problem ["normalise","polynomial",
7.5 "univariate","equation"])*)
7.6 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
7.7 - (* Specify_Method["PolyEq","normalize_poly"]*)
7.8 + (* Specify_Method["PolyEq","normalise_poly"]*)
7.9 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
7.10 - (*Apply_Method["PolyEq","normalize_poly"]*)
7.11 + (*Apply_Method["PolyEq","normalise_poly"]*)
7.12 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
7.13 (*Rewrite ("all_left","PolyEq.all_left")*)
7.14 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
7.15 @@ -1412,9 +1412,9 @@
7.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.17 (*Specify_Problem ["normalise","polynomial","univariate","equation"]*)
7.18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.19 - (*Specify_Method ["PolyEq", "normalize_poly"]*)
7.20 + (*Specify_Method ["PolyEq", "normalise_poly"]*)
7.21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.22 - (*Apply_Method ["PolyEq", "normalize_poly"]*)
7.23 + (*Apply_Method ["PolyEq", "normalise_poly"]*)
7.24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.25 (*Rewrite ("all_left", "PolyEq.all_left")*)
7.26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue Feb 13 16:17:59 2018 +0100
8.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Feb 14 06:06:27 2018 +0100
8.3 @@ -1480,12 +1480,12 @@
8.4 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.5 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Theory\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.6 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.7 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
8.8 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
8.9 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.10 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.11 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.12 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.13 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.14 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.15 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.16 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.17 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{2E}{\isachardot}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.18 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.19 @@ -1519,7 +1519,7 @@
8.20 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Check{\isaliteral{5F}{\isacharunderscore}}Postcond\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
8.21 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.22 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.23 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Check{\isaliteral{5F}{\isacharunderscore}}Postcond\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
8.24 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Check{\isaliteral{5F}{\isacharunderscore}}Postcond\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
8.25 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.26 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.27 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}End{\isaliteral{5F}{\isacharunderscore}}Proof{\isaliteral{27}{\isacharprime}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.28 @@ -2527,11 +2527,11 @@
8.29 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.30 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.31 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.32 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.33 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.34 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.35 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.36 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.37 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.38 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalize{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.39 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.40 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
8.41 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{2E}{\isachardot}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
8.42 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
9.1 --- a/test/Tools/isac/Frontend/use-cases.sml Tue Feb 13 16:17:59 2018 +0100
9.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Wed Feb 14 06:06:27 2018 +0100
9.3 @@ -615,9 +615,9 @@
9.4 setNextTactic 1 (Specify_Problem ["normalise","polynomial",
9.5 "univariate","equation"]);
9.6 autoCalculate 1 (Step 1); fetchProposedTactic 1;
9.7 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
9.8 + setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
9.9 autoCalculate 1 (Step 1); fetchProposedTactic 1;
9.10 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
9.11 + setNextTactic 1 (Apply_Method ["PolyEq","normalise_poly"]);
9.12 autoCalculate 1 (Step 1); fetchProposedTactic 1;
9.13 setNextTactic 1 (Rewrite ("all_left", num_str @{thm all_left}));
9.14 autoCalculate 1 (Step 1); fetchProposedTactic 1;
9.15 @@ -742,11 +742,11 @@
9.16 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
9.17
9.18 fetchProposedTactic 1;
9.19 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
9.20 + setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
9.21 autoCalculate 1 (Step 1);
9.22
9.23 fetchProposedTactic 1;
9.24 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
9.25 + setNextTactic 1 (Apply_Method ["PolyEq","normalise_poly"]);
9.26
9.27 autoCalculate 1 CompleteCalc;
9.28
9.29 @@ -765,7 +765,7 @@
9.30 autoCalculate 1 (Step 1);
9.31
9.32 fetchProposedTactic 1;
9.33 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
9.34 + setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
9.35 autoCalculate 1 (Step 1);
9.36
9.37 fetchProposedTactic 1;
10.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Tue Feb 13 16:17:59 2018 +0100
10.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Wed Feb 14 06:06:27 2018 +0100
10.3 @@ -109,7 +109,7 @@
10.4 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.5 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.6 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.7 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalize_poly"]*)
10.8 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
10.9 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.10 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.11 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.12 @@ -140,7 +140,7 @@
10.13 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.14 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.15 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.16 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalize_poly"]*)
10.17 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
10.18 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.19 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
10.20 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
11.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Feb 13 16:17:59 2018 +0100
11.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Feb 14 06:06:27 2018 +0100
11.3 @@ -340,11 +340,11 @@
11.4 ### assod: NotAss m= Subproblem' ,
11.5 stac= Substitute
11.6 [(b, (rhs o hd)
11.7 - (Subproblem (thy, [normalize, polynomial, univariate, equation])))]
11.8 + (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
11.9 (hd (filterVar A [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]))
11.10 *** stac2tac_ TODO: no match for Substitute
11.11 *** [(b, (rhs o hd)
11.12 -*** (Subproblem (thy, [normalize, polynomial, univariate, equation])))]
11.13 +*** (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
11.14 *** (hd (filterVar A [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]))
11.15 Exception- ERROR raised
11.16
11.17 @@ -364,7 +364,7 @@
11.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.21 -(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
11.22 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalise_poly"])*)
11.23
11.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.25 (*val f = Form' (FormKF (~1,EdUndef,3,Nundef,"A = a * b"))*)
12.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Feb 13 16:17:59 2018 +0100
12.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Feb 14 06:06:27 2018 +0100
12.3 @@ -10,15 +10,15 @@
12.4 "----------- occur_exactly_in ------------------------------------";
12.5 "----------- problems --------------------------------------------";
12.6 "----------- rewrite-order ord_simplify_System -------------------";
12.7 -"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
12.8 -"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
12.9 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
12.10 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
12.11 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
12.12 -"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
12.13 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
12.14 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
12.15 "----------- refine [linear,system]-------------------------------";
12.16 "----------- refine [2x2,linear,system] search error--------------";
12.17 -"----------- me [EqSystem,normalize,2x2] -------------------------";
12.18 -"----------- me [linear,system] ..normalize..top_down_sub..-------";
12.19 +"----------- me [EqSystem,normalise,2x2] -------------------------";
12.20 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
12.21 "----------- all systems from Biegelinie -------------------------";
12.22 "----------- 4x4 systems from Biegelinie -------------------------";
12.23 "-----------------------------------------------------------------";
12.24 @@ -145,9 +145,9 @@
12.25 then () else error "integrate.sml, (. * .) < (. * .) not#6";
12.26
12.27
12.28 -"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
12.29 -"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
12.30 -"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
12.31 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
12.32 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
12.33 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
12.34 val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\
12.35 \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
12.36 val bdvs = [(str2term"bdv_1",str2term"c"),
12.37 @@ -169,9 +169,9 @@
12.38 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
12.39 "--- 4---";
12.40
12.41 -"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
12.42 -"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
12.43 -"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
12.44 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
12.45 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
12.46 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
12.47 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
12.48 val t =
12.49 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
12.50 @@ -234,10 +234,10 @@
12.51 trace_rewrite:=false;
12.52
12.53
12.54 -"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
12.55 -"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
12.56 -"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
12.57 -(*STOPPED.WN06?: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
12.58 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
12.59 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
12.60 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
12.61 +(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
12.62 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
12.63 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
12.64 \c + c_2 + c_3 + c_4 = 0,\
12.65 @@ -328,7 +328,7 @@
12.66 Correct "solveForVars [c, c_2]"],
12.67 Where = [],
12.68 Relate = []})] => ()
12.69 -| _ => error "eqsystem.sml refine ['normalize','2x2'...]";
12.70 +| _ => error "eqsystem.sml refine ['normalise','2x2'...]";
12.71
12.72 "===== case 2 =====";
12.73 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
12.74 @@ -504,9 +504,9 @@
12.75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
12.76 *)
12.77
12.78 -"----------- me [EqSystem,normalize,2x2] -------------------------";
12.79 -"----------- me [EqSystem,normalize,2x2] -------------------------";
12.80 -"----------- me [EqSystem,normalize,2x2] -------------------------";
12.81 +"----------- me [EqSystem,normalise,2x2] -------------------------";
12.82 +"----------- me [EqSystem,normalise,2x2] -------------------------";
12.83 +"----------- me [EqSystem,normalise,2x2] -------------------------";
12.84 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
12.85 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
12.86 "solveForVars [c, c_2]", "solution LL"];
12.87 @@ -520,7 +520,7 @@
12.88 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.89 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.90 case nxt of ("Specify_Method",_) => ()
12.91 - | _ => error "eqsystem.sml [EqSystem,normalize,2x2] specify";
12.92 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
12.93
12.94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.95 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
12.96 @@ -530,7 +530,7 @@
12.97 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
12.98 case nxt of
12.99 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
12.100 - | _ => error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
12.101 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
12.102
12.103 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.104 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.105 @@ -567,9 +567,9 @@
12.106 (_, End_Proof') => ()
12.107 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
12.108
12.109 -"----------- me [linear,system] ..normalize..top_down_sub..-------";
12.110 -"----------- me [linear,system] ..normalize..top_down_sub..-------";
12.111 -"----------- me [linear,system] ..normalize..top_down_sub..-------";
12.112 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
12.113 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
12.114 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
12.115 val fmz =
12.116 ["equalities\
12.117 \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
12.118 @@ -765,9 +765,9 @@
12.119
12.120 val SOME (t, _) = rewrite_set_ thy false order_system t;
12.121 if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
12.122 -then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
12.123 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
12.124
12.125 -"----- 7.70 with met normalize: ";
12.126 +"----- 7.70 with met normalise: ";
12.127 val fmz = ["equalities" ^
12.128 "[L * q_0 = c, " ^
12.129 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^
12.130 @@ -792,7 +792,7 @@
12.131 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.132 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.133 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
12.134 - | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";
12.135 + | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
12.136 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.137
12.138 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
12.139 @@ -808,7 +808,7 @@
12.140 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.141 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.142 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
12.143 -then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
12.144 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
12.145 --------------------------------------------------------------------------*)
12.146
12.147 "----- 7.70 with met top_down_: me";
13.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Feb 13 16:17:59 2018 +0100
13.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Feb 14 06:06:27 2018 +0100
13.3 @@ -76,7 +76,7 @@
13.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.7 -(*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
13.8 +(*val nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
13.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.11 (* val nxt = (_,Subproblem ("PolyEq",["polynomial","univariate","equation"]=======*)
13.12 @@ -239,8 +239,8 @@
13.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.16 -case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) => ()
13.17 -| _ => error "55b normalize_poly specification broken";
13.18 +case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalise_poly"]) => ()
13.19 +| _ => error "55b normalise_poly specification broken";
13.20 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.21 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.23 @@ -251,7 +251,7 @@
13.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.25 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.26 case nxt of ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()
13.27 -| _ => error "55b normalize_poly specification broken";
13.28 +| _ => error "55b normalise_poly specification broken";
13.29 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.32 @@ -260,16 +260,16 @@
13.33 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
13.34 case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*)
13.35 if terms2str (get_assumptions_ pt p) =
13.36 -("[\"<not> matches (?a = 0)\n" ^
13.37 - " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^
13.38 - "<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^
13.39 - " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^
13.40 - "\"x = 6 / 5\"," ^
13.41 - "\"x = 0\"," ^
13.42 - "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^
13.43 - "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"," ^
13.44 - "\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0\"," ^
13.45 - "\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]")
13.46 +("[\"\<not> matches (?a = 0)\n " ^
13.47 + "((3 + -1 * x + x ^^^ 2) * x =\n " ^
13.48 + "1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^
13.49 + "1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^
13.50 + "\"x = 6 / 5\"," ^
13.51 + "\"x = 0\"," ^
13.52 + "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^
13.53 + "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"," ^
13.54 + "\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\"," ^
13.55 + "\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]")
13.56 then () else error "rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
13.57
13.58 (*
14.1 --- a/test/Tools/isac/Knowledge/rlang.sml Tue Feb 13 16:17:59 2018 +0100
14.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Feb 14 06:06:27 2018 +0100
14.3 @@ -522,7 +522,7 @@
14.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.7 -(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
14.8 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalise_poly"])*)
14.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.11 (*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
14.12 @@ -1698,7 +1698,7 @@
14.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.16 -(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
14.17 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalise_poly"])*)
14.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.20 (*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
14.21 @@ -1775,7 +1775,7 @@
14.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.25 -(*val nxt = Apply_Method ["PolyEq","normalize_poly"]) *)
14.26 +(*val nxt = Apply_Method ["PolyEq","normalise_poly"]) *)
14.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.29 (*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
15.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Tue Feb 13 16:17:59 2018 +0100
15.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Feb 14 06:06:27 2018 +0100
15.3 @@ -282,7 +282,7 @@
15.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.7 -(*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
15.8 +(*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalise_poly"])*)
15.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.11 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
15.12 @@ -334,7 +334,7 @@
15.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.16 -(*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
15.17 +(*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalise_poly"])*)
15.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.20 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
15.21 @@ -391,7 +391,7 @@
15.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.25 -(*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
15.26 +(*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalise_poly"])*)
15.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.29 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
16.1 --- a/test/Tools/isac/Knowledge/rootrat.sml Tue Feb 13 16:17:59 2018 +0100
16.2 +++ b/test/Tools/isac/Knowledge/rootrat.sml Wed Feb 14 06:06:27 2018 +0100
16.3 @@ -48,7 +48,7 @@
16.4
16.5 val SOME (t,asm) = rewrite_set_ thy true rls ttt;
16.6 if term2str t =
16.7 -"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * (-1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
16.8 +"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * (-1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
16.9 (*"-1 * x = -1 + sqrt (1 ^^^ 2 - -8) | x = -1 * (-1 + -1 * sqrt (1 ^^^ 2 - -8))"*)
16.10 then () else error "val rls = calculate_Rational GOON";
16.11
17.1 --- a/test/Tools/isac/Knowledge/system.sml Tue Feb 13 16:17:59 2018 +0100
17.2 +++ b/test/Tools/isac/Knowledge/system.sml Wed Feb 14 06:06:27 2018 +0100
17.3 @@ -9,16 +9,16 @@
17.4 "-----------------------------------------------------------------";
17.5 "table of contents -----------------------------------------------";
17.6 "-----------------------------------------------------------------";
17.7 -"----------- normalize system ------------------------------------";
17.8 +"----------- normalise system ------------------------------------";
17.9 "----------- me --------------------------------------------------";
17.10 "-----------------------------------------------------------------";
17.11 "-----------------------------------------------------------------";
17.12 "-----------------------------------------------------------------";
17.13
17.14
17.15 -"----------- normalize system ------------------------------------";
17.16 -"----------- normalize system ------------------------------------";
17.17 -"----------- normalize system ------------------------------------";
17.18 +"----------- normalise system ------------------------------------";
17.19 +"----------- normalise system ------------------------------------";
17.20 +"----------- normalise system ------------------------------------";
17.21 val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
17.22 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
17.23 val SOME (t,_) = rewrite_set_ thy false norm_Poly t;
18.1 --- a/test/Tools/isac/Test_Isac.thy Tue Feb 13 16:17:59 2018 +0100
18.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Feb 14 06:06:27 2018 +0100
18.3 @@ -195,6 +195,15 @@
18.4 ML_file "Knowledge/atools.sml"
18.5 ML_file "Knowledge/simplify.sml"
18.6 ML_file "Knowledge/poly.sml"
18.7 + ML_file "Knowledge/gcd_poly_ml.sml"
18.8 + ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
18.9 + ML_file "Knowledge/rational.sml"
18.10 + ML_file "Knowledge/equation.sml"
18.11 + ML_file "Knowledge/root.sml"
18.12 + ML_file "Knowledge/lineq.sml"
18.13 +(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
18.14 + ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
18.15 + ML_file "Knowledge/rootrat.sml"
18.16
18.17 ML {*
18.18 "~~~~~ fun xxx, args:"; val () = ();
18.19 @@ -203,17 +212,8 @@
18.20 *} ML {*
18.21 *}
18.22
18.23 - ML_file "Knowledge/gcd_poly_ml.sml"
18.24 - ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
18.25 - ML_file "Knowledge/rational.sml"
18.26 + ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
18.27 (*---------------------- check test file by testfile -------------------------------------------
18.28 - ML_file "Knowledge/equation.sml"
18.29 - ML_file "Knowledge/root.sml"
18.30 - ML_file "Knowledge/lineq.sml"
18.31 -(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
18.32 - ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
18.33 - ML_file "Knowledge/rootrat.sml"
18.34 - ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
18.35 ML_file "Knowledge/partial_fractions.sml"
18.36 ML_file "Knowledge/polyeq.sml"
18.37 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)