src/Tools/isac/Knowledge/Biegelinie.thy
branchdecompose-isar
changeset 42211 51c3c007d7fd
parent 41919 c85b0a1916a5
child 42385 b37adb659ffe
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Jul 26 16:50:27 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Jul 27 09:30:15 2011 +0200
     1.3 @@ -56,16 +56,16 @@
     1.4  	                        bool list] => bool list"	
     1.5  	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
     1.6  
     1.7 -axiomatization where
     1.8 +axioms(*axiomatization where*)
     1.9  
    1.10 -  Querkraft_Belastung:   "Q' x = -q_ x" and
    1.11 -  Belastung_Querkraft:   "-q_ x = Q' x" and
    1.12 +  Querkraft_Belastung:   "Q' x = -q_ x" (*and*)
    1.13 +  Belastung_Querkraft:   "-q_ x = Q' x" (*and*)
    1.14  
    1.15 -  Moment_Querkraft:      "M_b' x = Q x" and
    1.16 -  Querkraft_Moment:      "Q x = M_b' x" and
    1.17 +  Moment_Querkraft:      "M_b' x = Q x" (*and*)
    1.18 +  Querkraft_Moment:      "Q x = M_b' x" (*and*)
    1.19  
    1.20 -  Neigung_Moment:        "y'' x = -M_b x/ EI" and
    1.21 -  Moment_Neigung:        "M_b x = -EI * y'' x" and
    1.22 +  Neigung_Moment:        "y'' x = -M_b x/ EI" (*and*)
    1.23 +  Moment_Neigung:        "M_b x = -EI * y'' x" (*and*)
    1.24  
    1.25    (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
    1.26    make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"