1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -878,12 +878,12 @@
     1.4  section \<open>A problem for simplification of rationals\<close>
     1.5  setup \<open>KEStore_Elems.add_pbts
     1.6    [(Problem.prep_input thy "pbl_simp_rat" [] Problem.id_empty
     1.7 -      (["rational","simplification"],
     1.8 +      (["rational", "simplification"],
     1.9          [("#Given" ,["Term t_t"]),
    1.10            ("#Where" ,["t_t is_ratpolyexp"]),
    1.11            ("#Find"  ,["normalform n_n"])],
    1.12          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.13 -        SOME "Simplify t_t", [["simplification","of_rationals"]]))]\<close>
    1.14 +        SOME "Simplify t_t", [["simplification", "of_rationals"]]))]\<close>
    1.15  
    1.16  section \<open>A methods for simplification of rationals\<close>
    1.17  (*WN061025 this methods script is copied from (auto-generated) script
    1.18 @@ -906,7 +906,7 @@
    1.19     term)"
    1.20  setup \<open>KEStore_Elems.add_mets
    1.21      [Method.prep_input thy "met_simp_rat" [] Method.id_empty
    1.22 -      (["simplification","of_rationals"],
    1.23 +      (["simplification", "of_rationals"],
    1.24          [("#Given" ,["Term t_t"]),
    1.25            ("#Where" ,["t_t is_ratpolyexp"]),
    1.26            ("#Find"  ,["normalform n_n"])],