1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Apr 18 18:57:37 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Apr 24 17:44:02 2012 +0200
     1.3 @@ -80,19 +80,19 @@
     1.4  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
     1.5  store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] 
     1.6  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
     1.7 -store_thm thy ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
     1.8 +store_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
     1.9  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.10 -store_thm thy ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.11 +store_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.12  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.13 -store_thm thy ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.14 +store_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.15  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.16 -store_thm thy ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.17 +store_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.18  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.19 -store_thm thy ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.20 +store_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.21  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.22 -store_thm thy ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    1.23 +store_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    1.24  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.25 -store_thm thy ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    1.26 +store_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    1.27  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.28  
    1.29  *}