1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Jun 04 16:35:11 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Jun 04 17:20:40 2014 +0200
     1.3 @@ -74,28 +74,28 @@
     1.4  val thy = @{theory};
     1.5  
     1.6  (** theory elements for transfer into html **)
     1.7 +store_thes 
     1.8 +  [make_thy @{theory}
     1.9 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.10 +  make_isa @{theory} ("IsacKnowledge", "Theorems")
    1.11 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.12 +  make_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
    1.13 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.14 +  make_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.15 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.16 +  make_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.17 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.18 +  make_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.19 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.20 +  make_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.21 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.22 +  make_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    1.23 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    1.24 +  make_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    1.25 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]
    1.26 +  ]
    1.27 +*}
    1.28  
    1.29 -store_isa ["IsacKnowledge"] [];
    1.30 -store_thy thy 
    1.31 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.32 -store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] 
    1.33 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.34 -store_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
    1.35 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.36 -store_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    1.37 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.38 -store_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    1.39 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.40 -store_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    1.41 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.42 -store_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    1.43 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.44 -store_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    1.45 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.46 -store_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    1.47 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
    1.48 -
    1.49 -*}
    1.50  (** problems **)
    1.51  setup {* KEStore_Elems.add_pbts
    1.52    [(prep_pbt thy "pbl_bieg" [] e_pblID