1.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Sun Apr 18 13:17:06 2021 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Sun Apr 18 15:19:49 2021 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4  "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
     1.5  "----------- fun Thm.make_thm ------------------------------------";
     1.6  "----------- correct theIDs for Rule_Set.empty -------------------";
     1.7 -"----------- fun revert_sym_rule --------------------------------------";
     1.8  "----------- fun thms_of_rlss ------------------------------------";
     1.9  "----------- repair thydata2xml for rls --------------------------";
    1.10  "----------- fun get_fun_ids -------------------------------------------------------------------";
    1.11 @@ -169,22 +168,6 @@
    1.12                                                  ["IsacScripts", "Know_Store", "Rulesets", "empty"], 
    1.13    :*)
    1.14  
    1.15 -"----------- fun revert_sym_rule --------------------------------------";
    1.16 -"----------- fun revert_sym_rule --------------------------------------";
    1.17 -"----------- fun revert_sym_rule --------------------------------------";
    1.18 -val thy = @{theory Isac_Knowledge}
    1.19 -val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    1.20 -  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
    1.21 -;
    1.22 -if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
    1.23 -then () else error "fun revert_sym_rule changed 1";
    1.24 -
    1.25 -val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    1.26 -  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    1.27 -;
    1.28 -if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
    1.29 -then () else error "fun revert_sym_rule changed 2"
    1.30 -
    1.31  "----------- fun thms_of_rlss ------------------------------------";
    1.32  "----------- fun thms_of_rlss ------------------------------------";
    1.33  "----------- fun thms_of_rlss ------------------------------------";

     2.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml	Sun Apr 18 13:17:06 2021 +0200
     2.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml	Sun Apr 18 15:19:49 2021 +0200
     2.3 @@ -6,12 +6,37 @@
     2.4  "-----------------------------------------------------------------------------------------------";
     2.5  "table of contents -----------------------------------------------------------------------------";
     2.6  "-----------------------------------------------------------------------------------------------";
     2.7 -"----------- TODO ------------------------------------------------------------------------------";
     2.8 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
     2.9  "-----------------------------------------------------------------------------------------------";
    2.10  "-----------------------------------------------------------------------------------------------";
    2.11  "-----------------------------------------------------------------------------------------------";
    2.12  
    2.13  
    2.14 -"----------- TODO ------------------------------------------------------------------------------";
    2.15 -"----------- TODO ------------------------------------------------------------------------------";
    2.16 -"----------- TODO ------------------------------------------------------------------------------";
    2.17 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
    2.18 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
    2.19 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
    2.20 +"~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
    2.21 +  (@{theory Isac_Knowledge},
    2.22 +    Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
    2.23 +
    2.24 +if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
    2.25 +else error "input to revert_sym_rule CHANGED";
    2.26 +
    2.27 +      (*if*) is_sym (cut_id id) (*then*);
    2.28 +          val id' = id_drop_sym id
    2.29 +          val thm' = thm_from_thy thy id'
    2.30 +          val id'' = Thm.get_name_hint thm'
    2.31 +(*GOON*)
    2.32 +
    2.33 +val thy = @{theory Isac_Knowledge}
    2.34 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    2.35 +  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
    2.36 +;
    2.37 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
    2.38 +then () else error "fun revert_sym_rule changed 1";
    2.39 +
    2.40 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    2.41 +  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    2.42 +;
    2.43 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
    2.44 +then () else error "fun revert_sym_rule changed 2"