1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Wed Feb 07 13:06:27 2018 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Wed Feb 07 15:00:37 2018 +0100
     1.3 @@ -624,9 +624,9 @@
     1.4    BUT WE FIND IN THE CODE ABOVE IN next_tac:*)
     1.5  ;
     1.6  (*----------------------------------------------------------------------------------------------*)
     1.7 -if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
     1.8 +if string_of_thmI @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
     1.9  then () else error "string_of_thmI changed";
    1.10 -if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
    1.11 +if string_of_thm @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
    1.12  then () else error "string_of_thm changed";
    1.13  (*----------------------------------------------------------------------------------------------*)
    1.14  ;