1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Mar 15 15:48:52 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Mar 23 10:14:39 2018 +0100
1.3 @@ -294,7 +294,7 @@
1.4 ML {*
1.5 val isolate_bdvs =
1.6 Celem.Rls {id="isolate_bdvs", preconds = [],
1.7 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.8 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.9 erls = Celem.append_rls "erls_isolate_bdvs" Celem.e_rls
1.10 [(Celem.Calc ("EqSystem.occur'_exactly'_in",
1.11 eval_occur_exactly_in
1.12 @@ -310,7 +310,7 @@
1.13 ML {*
1.14 val isolate_bdvs_4x4 =
1.15 Celem.Rls {id="isolate_bdvs_4x4", preconds = [],
1.16 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.17 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.18 erls = Celem.append_rls
1.19 "erls_isolate_bdvs_4x4" Celem.e_rls
1.20 [Celem.Calc ("EqSystem.occur'_exactly'_in",
1.21 @@ -345,9 +345,9 @@
1.22
1.23 val prls_triangular =
1.24 Celem.Rls {id="prls_triangular", preconds = [],
1.25 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.26 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.27 erls = Celem.Rls {id="erls_prls_triangular", preconds = [],
1.28 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.29 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.30 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.31 rules = [(*for precond NTH_CONS ...*)
1.32 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.33 @@ -374,9 +374,9 @@
1.34 more similarity to prls_triangular desirable*)
1.35 val prls_triangular4 =
1.36 Celem.Rls {id="prls_triangular4", preconds = [],
1.37 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.38 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.39 erls = Celem.Rls {id="erls_prls_triangular4", preconds = [],
1.40 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
1.41 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.42 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.43 rules = [(*for precond NTH_CONS ...*)
1.44 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.45 @@ -416,13 +416,13 @@
1.46 (["system"],
1.47 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.48 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
1.49 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.50 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.51 (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
1.52 (["LINEAR", "system"],
1.53 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.54 (*TODO.WN050929 check linearity*)
1.55 ("#Find" ,["solution ss'''"])],
1.56 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.57 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.58 (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
1.59 (["2x2", "LINEAR", "system"],
1.60 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.61 @@ -447,7 +447,7 @@
1.62 (["normalise", "2x2", "LINEAR", "system"],
1.63 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.64 ("#Find" ,["solution ss'''"])],
1.65 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
1.66 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.67 SOME "solveSystem e_s v_s",
1.68 [["EqSystem","normalise","2x2"]])),
1.69 (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
1.70 @@ -492,7 +492,7 @@
1.71 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.72 (*LENGTH is checked 1 level above*)
1.73 ("#Find" ,["solution ss'''"])],
1.74 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
1.75 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.76 SOME "solveSystem e_s v_s",
1.77 [["EqSystem","normalise","4x4"]]))] *}
1.78