1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Oct 05 12:22:51 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Oct 06 12:42:25 2020 +0200
     1.3 @@ -8,13 +8,12 @@
     1.4  
     1.5  section \<open>Constants specific for Biegelinie\<close>
     1.6  
     1.7 -(*/----- exception FAIL NONE raised (line 161 of "General/scan.ML") ---------------------------\
     1.8  consts
     1.9    qq    :: "real => real"             (* Streckenlast               *)
    1.10    Q     :: "real => real"             (* Querkraft                  *)
    1.11    Q'    :: "real => real"             (* Ableitung der Querkraft    *)
    1.12    M'_b  :: "real => real" ("M'_b")    (* Biegemoment                *)
    1.13 -  M'_b' :: "real => real" ("M'_b'")   (* Ableitung des Biegemoments *)
    1.14 +(*M'_b' :: "real => real" ("M'_b' ")  ( * Ableitung des Biegemoments, Unused*)
    1.15    y''   :: "real => real"             (* 2.Ableitung der Biegeline  *)
    1.16    y'    :: "real => real"             (* Neigung der Biegeline      *)
    1.17  (*y     :: "real => real"             (* Biegeline                  *)*)
    1.18 @@ -50,8 +49,8 @@
    1.19    Moment_Querkraft:      "M_b' x = Q x" and
    1.20    Querkraft_Moment:      "Q x = M_b' x" and
    1.21  
    1.22 -  Neigung_Moment:        "y'' x = -M_b x/ EI" and
    1.23 -  Moment_Neigung:        "M_b x = -EI * y'' x" and
    1.24 +  Neigung_Moment:        "y'' x = -M_b (x / EI)" and
    1.25 +  Moment_Neigung:        "(M_b x) = -EI * y'' x" and
    1.26  
    1.27    (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
    1.28    make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
    1.29 @@ -383,7 +382,6 @@
    1.30  ML \<open>
    1.31  \<close> ML \<open>
    1.32  \<close>
    1.33 -  \----- exception FAIL NONE raised (line 161 of "General/scan.ML") ---------------------------/*)
    1.34  
    1.35  end
    1.36  

     2.1 --- a/test/Pure/Isar/Theory_Commands.thy	Mon Oct 05 12:22:51 2020 +0200
     2.2 +++ b/test/Pure/Isar/Theory_Commands.thy	Tue Oct 06 12:42:25 2020 +0200
     2.3 @@ -45,7 +45,7 @@
     2.4  (*da*)  end)
     2.5    end
     2.6  \<close>
     2.7 -(*legend: "da":
     2.8 +(*"da" legend:
     2.9    same as "theory_text_antiquotation", etc in src/Pure/Thy/document_antiquotations.ML
    2.10  
    2.11    cited from Makarius' mail: