1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jul 31 16:55:22 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Aug 04 15:54:57 2014 +0200
     1.3 @@ -76,19 +76,19 @@
     1.4      ["Walther Neuper 2005 supported by a grant from NMI Austria"],
     1.5    make_isa @{theory} ("IsacKnowledge", "Theorems")
     1.6      ["Walther Neuper 2005 supported by a grant from NMI Austria"],
     1.7 -  make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
     1.8 +  make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
     1.9  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.10 -  make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.11 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
    1.12  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.13 -  make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.14 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
    1.15  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.16 -  make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.17 +  make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
    1.18  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.19 -  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.20 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
    1.21  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.22 -  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    1.23 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
    1.24  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.25 -  make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    1.26 +  make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
    1.27  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
    1.28  *}
    1.29