src/Tools/isac/Knowledge/Biegelinie.thy
changeset 52148 aabc6c8e930a
parent 42451 bc03b5d60547
child 55276 ce872d7781d2
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Fri Oct 18 14:36:51 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Oct 21 09:03:50 2013 +0200
     1.3 @@ -56,16 +56,16 @@
     1.4  	                        bool list] => bool list"	
     1.5  	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
     1.6  
     1.7 -axioms(*axiomatization where*)
     1.8 +axiomatization where
     1.9  
    1.10 -  Querkraft_Belastung:   "Q' x = -qq x" (*and*)
    1.11 -  Belastung_Querkraft:   "-qq x = Q' x" (*and*)
    1.12 +  Querkraft_Belastung:   "Q' x = -qq x" and
    1.13 +  Belastung_Querkraft:   "-qq 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)"