src/Tools/isac/Knowledge/EqSystem.thy
changeset 60449 2406d378cede
parent 60377 4f5f29fd0af9
child 60506 145e45cd7a0f
     1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4  
     1.5  problem pbl_equsys_lin_2x2_tri : "triangular/2x2/LINEAR/system" =
     1.6    \<open>prls_triangular\<close>
     1.7 -  Method: "EqSystem/top_down_substitution/2x2"
     1.8 +  Method_Ref: "EqSystem/top_down_substitution/2x2"
     1.9    CAS: "solveSystem e_s v_s"
    1.10    Given: "equalities e_s" "solveForVars v_s"
    1.11    Where:
    1.12 @@ -413,7 +413,7 @@
    1.13  
    1.14  problem pbl_equsys_lin_2x2_norm : "normalise/2x2/LINEAR/system" =
    1.15    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.16 -  Method: "EqSystem/normalise/2x2"
    1.17 +  Method_Ref: "EqSystem/normalise/2x2"
    1.18    CAS: "solveSystem e_s v_s"
    1.19    Given: "equalities e_s" "solveForVars v_s"
    1.20    Find: "solution ss'''"
    1.21 @@ -443,7 +443,7 @@
    1.22  problem pbl_equsys_lin_4x4_tri : "triangular/4x4/LINEAR/system" =
    1.23    \<open>Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
    1.24      [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")]\<close>
    1.25 -  Method: "EqSystem/top_down_substitution/4x4"
    1.26 +  Method_Ref: "EqSystem/top_down_substitution/4x4"
    1.27    CAS: "solveSystem e_s v_s"
    1.28    Given: "equalities e_s" "solveForVars v_s"
    1.29    Where: (*accepts missing variables up to diagional form*)
    1.30 @@ -455,7 +455,7 @@
    1.31  
    1.32  problem pbl_equsys_lin_4x4_norm : "normalise/4x4/LINEAR/system" =
    1.33    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.34 -  Method: "EqSystem/normalise/4x4"
    1.35 +  Method_Ref: "EqSystem/normalise/4x4"
    1.36    CAS: "solveSystem e_s v_s"
    1.37    Given: "equalities e_s" "solveForVars v_s"
    1.38    (*Length is checked 1 level above*)