1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Dec 02 12:32:30 2020 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Dec 07 17:39:21 2020 +0100
     1.3 @@ -423,7 +423,7 @@
     1.4        (["2x2", "LINEAR", "system"],
     1.5        (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
     1.6          [("#Given" ,["equalities e_s", "solveForVars v_s"]),
     1.7 -          ("#Where"  ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
     1.8 +          ("#Where"  ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
     1.9            ("#Find"  ,["solution ss'''"])],
    1.10          Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty 
    1.11  			    [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
    1.12 @@ -450,7 +450,7 @@
    1.13        (["3x3", "LINEAR", "system"],
    1.14          (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.15          [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.16 -          ("#Where"  ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
    1.17 +          ("#Where"  ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
    1.18            ("#Find"  ,["solution ss'''"])],
    1.19          Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty 
    1.20  			    [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
    1.21 @@ -462,7 +462,7 @@
    1.22        (["4x4", "LINEAR", "system"],
    1.23          (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.24          [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.25 -          ("#Where"  ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
    1.26 +          ("#Where"  ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
    1.27            ("#Find"  ,["solution ss'''"])],
    1.28          Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty 
    1.29  			    [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
    1.30 @@ -486,7 +486,7 @@
    1.31      (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
    1.32        (["normalise", "4x4", "LINEAR", "system"],
    1.33          [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.34 -          (*LENGTH is checked 1 level above*)
    1.35 +          (*Length is checked 1 level above*)
    1.36            ("#Find"  ,["solution ss'''"])],
    1.37          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.38          SOME "solveSystem e_s v_s",