1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Sep 01 16:15:13 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Sep 01 16:43:58 2010 +0200
1.3 @@ -72,33 +72,35 @@
1.4 make_fun_explicit "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
1.5
1.6 ML {*
1.7 +val thy = @{theory};
1.8 +
1.9 (** theory elements for transfer into html **)
1.10
1.11 store_isa ["IsacKnowledge"] [];
1.12 -store_thy (theory "Biegelinie")
1.13 +store_thy thy
1.14 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.15 -store_isa ["IsacKnowledge", theory2thyID (theory "Biegelinie"), "Theorems"]
1.16 +store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
1.17 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.18 -store_thm (theory "Biegelinie") ("Belastung_Querkraft", Belastung_Querkraft)
1.19 +store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)
1.20 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.21 -store_thm (theory "Biegelinie") ("Moment_Neigung", Moment_Neigung)
1.22 +store_thm thy ("Moment_Neigung", Moment_Neigung)
1.23 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.24 -store_thm (theory "Biegelinie") ("Moment_Querkraft", Moment_Querkraft)
1.25 +store_thm thy ("Moment_Querkraft", Moment_Querkraft)
1.26 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.27 -store_thm (theory "Biegelinie") ("Neigung_Moment", Neigung_Moment)
1.28 +store_thm thy ("Neigung_Moment", Neigung_Moment)
1.29 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.30 -store_thm (theory "Biegelinie") ("Querkraft_Belastung", Querkraft_Belastung)
1.31 +store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)
1.32 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.33 -store_thm (theory "Biegelinie") ("Querkraft_Moment", Querkraft_Moment)
1.34 +store_thm thy ("Querkraft_Moment", Querkraft_Moment)
1.35 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.36 -store_thm (theory "Biegelinie") ("make_fun_explicit", make_fun_explicit)
1.37 +store_thm thy ("make_fun_explicit", make_fun_explicit)
1.38 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.39
1.40
1.41 (** problems **)
1.42
1.43 store_pbt
1.44 - (prep_pbt (theory "Biegelinie") "pbl_bieg" [] e_pblID
1.45 + (prep_pbt thy "pbl_bieg" [] e_pblID
1.46 (["Biegelinien"],
1.47 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.48 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.49 @@ -110,7 +112,7 @@
1.50 [["IntegrierenUndKonstanteBestimmen2"]]));
1.51
1.52 store_pbt
1.53 - (prep_pbt (theory "Biegelinie") "pbl_bieg_mom" [] e_pblID
1.54 + (prep_pbt thy "pbl_bieg_mom" [] e_pblID
1.55 (["MomentBestimmte","Biegelinien"],
1.56 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.57 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.58 @@ -122,7 +124,7 @@
1.59 [["IntegrierenUndKonstanteBestimmen"]]));
1.60
1.61 store_pbt
1.62 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momg" [] e_pblID
1.63 + (prep_pbt thy "pbl_bieg_momg" [] e_pblID
1.64 (["MomentGegebene","Biegelinien"],
1.65 [],
1.66 append_rls "e_rls" e_rls [],
1.67 @@ -130,7 +132,7 @@
1.68 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
1.69
1.70 store_pbt
1.71 - (prep_pbt (theory "Biegelinie") "pbl_bieg_einf" [] e_pblID
1.72 + (prep_pbt thy "pbl_bieg_einf" [] e_pblID
1.73 (["einfache","Biegelinien"],
1.74 [],
1.75 append_rls "e_rls" e_rls [],
1.76 @@ -138,7 +140,7 @@
1.77 [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
1.78
1.79 store_pbt
1.80 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momquer" [] e_pblID
1.81 + (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
1.82 (["QuerkraftUndMomentBestimmte","Biegelinien"],
1.83 [],
1.84 append_rls "e_rls" e_rls [],
1.85 @@ -146,7 +148,7 @@
1.86 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
1.87
1.88 store_pbt
1.89 - (prep_pbt (theory "Biegelinie") "pbl_bieg_vonq" [] e_pblID
1.90 + (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
1.91 (["vonBelastungZu","Biegelinien"],
1.92 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.93 ("#Find" ,["Funktionen funs___"])],
1.94 @@ -155,7 +157,7 @@
1.95 [["Biegelinien","ausBelastung"]]));
1.96
1.97 store_pbt
1.98 - (prep_pbt (theory "Biegelinie") "pbl_bieg_randbed" [] e_pblID
1.99 + (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
1.100 (["setzeRandbedingungen","Biegelinien"],
1.101 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.102 ("#Find" ,["Gleichungen equs___"])],
1.103 @@ -164,7 +166,7 @@
1.104 [["Biegelinien","setzeRandbedingungenEin"]]));
1.105
1.106 store_pbt
1.107 - (prep_pbt (theory "Biegelinie") "pbl_equ_fromfun" [] e_pblID
1.108 + (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
1.109 (["makeFunctionTo","equation"],
1.110 [("#Given" ,["functionEq fun_","substitution sub_"]),
1.111 ("#Find" ,["equality equ___"])],
1.112 @@ -223,7 +225,7 @@
1.113 scr = EmptyScr};
1.114
1.115 store_met
1.116 - (prep_met (theory "Biegelinie") "met_biege" [] e_metID
1.117 + (prep_met thy "met_biege" [] e_metID
1.118 (["IntegrierenUndKonstanteBestimmen"],
1.119 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.120 "FunktionsVariable v_"]),
1.121 @@ -301,7 +303,7 @@
1.122 ));
1.123
1.124 store_met
1.125 - (prep_met (theory "Biegelinie") "met_biege_2" [] e_metID
1.126 + (prep_met thy "met_biege_2" [] e_metID
1.127 (["IntegrierenUndKonstanteBestimmen2"],
1.128 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.129 "FunktionsVariable v_"]),
1.130 @@ -344,7 +346,7 @@
1.131 ));
1.132
1.133 store_met
1.134 - (prep_met (theory "Biegelinie") "met_biege_intconst_2" [] e_metID
1.135 + (prep_met thy "met_biege_intconst_2" [] e_metID
1.136 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.137 [],
1.138 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.139 @@ -355,7 +357,7 @@
1.140 ));
1.141
1.142 store_met
1.143 - (prep_met (theory "Biegelinie") "met_biege_intconst_4" [] e_metID
1.144 + (prep_met thy "met_biege_intconst_4" [] e_metID
1.145 (["IntegrierenUndKonstanteBestimmen","4x4System"],
1.146 [],
1.147 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.148 @@ -366,7 +368,7 @@
1.149 ));
1.150
1.151 store_met
1.152 - (prep_met (theory "Biegelinie") "met_biege_intconst_1" [] e_metID
1.153 + (prep_met thy "met_biege_intconst_1" [] e_metID
1.154 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
1.155 [],
1.156 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.157 @@ -377,7 +379,7 @@
1.158 ));
1.159
1.160 store_met
1.161 - (prep_met (theory "Biegelinie") "met_biege2" [] e_metID
1.162 + (prep_met thy "met_biege2" [] e_metID
1.163 (["Biegelinien"],
1.164 [],
1.165 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.166 @@ -388,7 +390,7 @@
1.167 ));
1.168
1.169 store_met
1.170 - (prep_met (theory "Biegelinie") "met_biege_ausbelast" [] e_metID
1.171 + (prep_met thy "met_biege_ausbelast" [] e_metID
1.172 (["Biegelinien","ausBelastung"],
1.173 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.174 ("#Find" ,["Funktionen funs_"])],
1.175 @@ -428,7 +430,7 @@
1.176 ));
1.177
1.178 store_met
1.179 - (prep_met (theory "Biegelinie") "met_biege_setzrand" [] e_metID
1.180 + (prep_met thy "met_biege_setzrand" [] e_metID
1.181 (["Biegelinien","setzeRandbedingungenEin"],
1.182 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.183 ("#Find" ,["Gleichungen equs___"])],
1.184 @@ -492,7 +494,7 @@
1.185 ));
1.186
1.187 store_met
1.188 - (prep_met (theory "Biegelinie") "met_equ_fromfun" [] e_metID
1.189 + (prep_met thy "met_equ_fromfun" [] e_metID
1.190 (["Equation","fromFunction"],
1.191 [("#Given" ,["functionEq fun_","substitution sub_"]),
1.192 ("#Find" ,["equality equ___"])],