1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -45,14 +45,14 @@
     1.4  setup \<open>KEStore_Elems.add_pbts
     1.5    [(Problem.prep_input thy "pbl_equ" [] Problem.id_empty
     1.6        (["equation"],
     1.7 -        [("#Given" ,["equality e_e","solveFor v_v"]),
     1.8 +        [("#Given" ,["equality e_e", "solveFor v_v"]),
     1.9            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.10            ("#Find"  ,["solutions v_v'i'"])],
    1.11          Rule_Set.append_rules "equation_prls" Rule_Set.empty  [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
    1.12          SOME "solve (e_e::bool, v_v)", [])),
    1.13      (Problem.prep_input thy "pbl_equ_univ" [] Problem.id_empty
    1.14 -      (["univariate","equation"],
    1.15 -        [("#Given" ,["equality e_e","solveFor v_v"]),
    1.16 +      (["univariate", "equation"],
    1.17 +        [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.18            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.19            ("#Find"  ,["solutions v_v'i'"])],
    1.20          univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
    1.21 @@ -75,9 +75,9 @@
    1.22  \<close>
    1.23  setup \<open>KEStore_Elems.add_cas
    1.24    [((Thm.term_of o the o (TermC.parse thy)) "solveTest", 
    1.25 -      (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
    1.26 +      (("Test", ["univariate", "equation", "test"], ["no_met"]), argl2dtss)),
    1.27      ((Thm.term_of o the o (TermC.parse thy)) "solve",
    1.28 -      (("Isac_Knowledge", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
    1.29 +      (("Isac_Knowledge", ["univariate", "equation"], ["no_met"]), argl2dtss))]\<close>
    1.30  
    1.31  
    1.32  setup \<open>KEStore_Elems.add_mets