1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 08:53:54 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 09:09:53 2014 +0200
     1.3 @@ -95,6 +95,27 @@
     1.4  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]
     1.5    ]
     1.6  *}
     1.7 +setup {*
     1.8 +KEStore_Elems.add_thes
     1.9 +  [make_thy @{theory}
    1.10 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.11 +  make_isa @{theory} ("IsacKnowledge", "Theorems")
    1.12 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.13 +  make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
    1.14 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.15 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.16 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.17 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.18 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.19 +  make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.20 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.21 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.22 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.23 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", prop_of @{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 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
    1.27 +*}
    1.28  
    1.29  (** problems **)
    1.30  setup {* KEStore_Elems.add_pbts