src/Tools/isac/Knowledge/Biegelinie.thy
branchisac-update-Isa09-2
changeset 37983 03bfbc480107
parent 37982 66f3570ba808
child 37984 972a73d7c50b
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -57,19 +57,19 @@
     1.4  	                        bool list] => bool list"	
     1.5  	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
     1.6  
     1.7 -rules
     1.8 +axioms
     1.9  
    1.10 -  Querkraft_Belastung   "Q' x = -q_ x"
    1.11 -  Belastung_Querkraft   "-q_ x = Q' x"
    1.12 +  Querkraft_Belastung:   "Q' x = -q_ x"
    1.13 +  Belastung_Querkraft:   "-q_ x = Q' x"
    1.14  
    1.15 -  Moment_Querkraft      "M_b' x = Q x"
    1.16 -  Querkraft_Moment      "Q x = M_b' x"
    1.17 +  Moment_Querkraft:      "M_b' x = Q x"
    1.18 +  Querkraft_Moment:      "Q x = M_b' x"
    1.19  
    1.20 -  Neigung_Moment        "y'' x = -M_b x/ EI"
    1.21 -  Moment_Neigung        "M_b x = -EI * y'' x"
    1.22 +  Neigung_Moment:        "y'' x = -M_b x/ EI"
    1.23 +  Moment_Neigung:        "M_b x = -EI * y'' x"
    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)"
    1.27 +  make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
    1.28  
    1.29  ML {*
    1.30  val thy = @{theory};