Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/AlgEin.thy
changeset 59489 cfcbcac0bae8
parent 59473 28b67cae58c3
child 59504 546bd1b027cc 
     1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Thu Dec 20 18:02:25 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Wed Dec 26 14:24:05 2018 +0100
     1.3 @@ -64,18 +64,18 @@
     1.4             "      t_t = Substitute [oben = su_m] t_t;                     " ^
     1.5             "      t_t = Substitute o_o t_t;                                " ^
     1.6             "      t_t = Substitute [k_k, q__q] t_t;                         " ^
     1.7 -           "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
     1.8 +           "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
     1.9             "      su_m = boollist2sum s_s;                               " ^
    1.10             "      t_t = Substitute [senkrecht = su_m] t_t;                " ^
    1.11             "      t_t = Substitute s_s t_t;                                " ^
    1.12             "      t_t = Substitute [k_k, q__q] t_t;                         " ^
    1.13 -           "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
    1.14 +           "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
    1.15             "      su_m = boollist2sum u_u;                               " ^
    1.16             "      t_t = Substitute [unten = su_m] t_t;                    " ^
    1.17             "      t_t = Substitute u_u t_t;                                " ^
    1.18             "      t_t = Substitute [k_k, q__q] t_t;                         " ^
    1.19 -           "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t  " ^
    1.20 -           " in (Try (Rewrite_Set norm_Poly False)) t_t)                  ")]
    1.21 +           "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t  " ^
    1.22 +           " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)                  ")]
    1.23  \<close>
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25      [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
    1.26 @@ -93,17 +93,17 @@
    1.27                "      su_m = boollist2sum o_o;                               " ^
    1.28                "      t_t = Substitute [oben = su_m] t_t;                     " ^
    1.29                "      t_t = Substitute o_o t_t;                                " ^
    1.30 -              "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
    1.31 +              "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
    1.32                "      su_m = boollist2sum s_s;                               " ^
    1.33                "      t_t = Substitute [senkrecht = su_m] t_t;                " ^
    1.34                "      t_t = Substitute s_s t_t;                                " ^
    1.35 -              "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
    1.36 +              "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
    1.37                "      su_m = boollist2sum u_u;                               " ^
    1.38                "      t_t = Substitute [unten = su_m] t_t;                    " ^
    1.39                "      t_t = Substitute u_u t_t;                                " ^
    1.40 -              "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
    1.41 +              "      t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
    1.42                "      t_t = Substitute [k_k, q__q] t_t                          " ^
    1.43 -              " in (Try (Rewrite_Set norm_Poly False)) t_t)                 ")]
    1.44 +              " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)                 ")]
    1.45  \<close>
    1.46  
    1.47  end
wneuper/isa