src/Tools/isac/Knowledge/Biegelinie.thy
branchdecompose-isar
changeset 41919 c85b0a1916a5
parent 41918 7e44a163ac1d
child 42211 51c3c007d7fd
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Mar 03 16:38:59 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Mar 03 17:37:46 2011 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4     (c) due to copyright terms
     1.5  *)
     1.6  
     1.7 -theory Biegelinie imports Integrate Equation EqSystem begin
     1.8 +theory Biegelinie imports Integrate Equation EqSystem Atools begin
     1.9  
    1.10  consts
    1.11  
    1.12 @@ -56,7 +56,7 @@
    1.13  	                        bool list] => bool list"	
    1.14  	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
    1.15  
    1.16 -axiomatization
    1.17 +axiomatization where
    1.18  
    1.19    Querkraft_Belastung:   "Q' x = -q_ x" and
    1.20    Belastung_Querkraft:   "-q_ x = Q' x" and