1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -94,14 +94,14 @@
1.4
1.5 (** problems **)
1.6 setup {* KEStore_Elems.add_pbts
1.7 - [(prep_pbt @{theory} "pbl_bieg" [] e_pblID
1.8 + [(Specify.prep_pbt @{theory} "pbl_bieg" [] e_pblID
1.9 (["Biegelinien"],
1.10 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.11 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.12 ("#Find" ,["Biegelinie b_b"]),
1.13 ("#Relate",["Randbedingungen r_b"])],
1.14 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
1.15 - (prep_pbt @{theory} "pbl_bieg_mom" [] e_pblID
1.16 + (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] e_pblID
1.17 (["MomentBestimmte","Biegelinien"],
1.18 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.19 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.20 @@ -109,26 +109,26 @@
1.21 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
1.22 ],
1.23 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
1.24 - (prep_pbt @{theory} "pbl_bieg_momg" [] e_pblID
1.25 + (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] e_pblID
1.26 (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.27 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
1.28 - (prep_pbt @{theory} "pbl_bieg_einf" [] e_pblID
1.29 + (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] e_pblID
1.30 (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.31 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
1.32 - (prep_pbt @{theory} "pbl_bieg_momquer" [] e_pblID
1.33 + (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] e_pblID
1.34 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.35 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
1.36 - (prep_pbt @{theory} "pbl_bieg_vonq" [] e_pblID
1.37 + (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] e_pblID
1.38 (["vonBelastungZu","Biegelinien"],
1.39 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
1.40 ("#Find" ,["Funktionen funs'''"])],
1.41 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
1.42 - (prep_pbt @{theory} "pbl_bieg_randbed" [] e_pblID
1.43 + (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] e_pblID
1.44 (["setzeRandbedingungen","Biegelinien"],
1.45 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.46 ("#Find" ,["Gleichungen equs'''"])],
1.47 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
1.48 - (prep_pbt @{theory} "pbl_equ_fromfun" [] e_pblID
1.49 + (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] e_pblID
1.50 (["makeFunctionTo","equation"],
1.51 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.52 ("#Find" ,["equality equ'''"])],
1.53 @@ -185,7 +185,7 @@
1.54 *}
1.55
1.56 setup {* KEStore_Elems.add_mets
1.57 - [prep_met @{theory} "met_biege" [] e_metID
1.58 + [Specify.prep_met @{theory} "met_biege" [] e_metID
1.59 (["IntegrierenUndKonstanteBestimmen"],
1.60 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.61 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.62 @@ -261,7 +261,7 @@
1.63 " B__B = ((Substitute c_1_2) @@ " ^
1.64 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.65 " in B__B)"),
1.66 - prep_met @{theory} "met_biege_2" [] e_metID
1.67 + Specify.prep_met @{theory} "met_biege_2" [] e_metID
1.68 (["IntegrierenUndKonstanteBestimmen2"],
1.69 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.70 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.71 @@ -298,27 +298,27 @@
1.72 " B_B = ((Substitute con_s) @@ " ^
1.73 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.74 " in B_B)"),
1.75 - prep_met @{theory} "met_biege_intconst_2" [] e_metID
1.76 + Specify.prep_met @{theory} "met_biege_intconst_2" [] e_metID
1.77 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
1.78 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.79 errpats = [], nrls = e_rls},
1.80 "empty_script"),
1.81 - prep_met @{theory} "met_biege_intconst_4" [] e_metID
1.82 + Specify.prep_met @{theory} "met_biege_intconst_4" [] e_metID
1.83 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
1.84 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.85 errpats = [], nrls = e_rls},
1.86 "empty_script"),
1.87 - prep_met @{theory} "met_biege_intconst_1" [] e_metID
1.88 + Specify.prep_met @{theory} "met_biege_intconst_1" [] e_metID
1.89 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
1.90 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.91 errpats = [], nrls = e_rls},
1.92 "empty_script"),
1.93 - prep_met @{theory} "met_biege2" [] e_metID
1.94 + Specify.prep_met @{theory} "met_biege2" [] e_metID
1.95 (["Biegelinien"], [],
1.96 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.97 errpats = [], nrls = e_rls},
1.98 "empty_script"),
1.99 - prep_met @{theory} "met_biege_ausbelast" [] e_metID
1.100 + Specify.prep_met @{theory} "met_biege_ausbelast" [] e_metID
1.101 (["Biegelinien", "ausBelastung"],
1.102 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.103 ("#Find" ,["Funktionen fun_s"])],
1.104 @@ -355,7 +355,7 @@
1.105 " [diff,integration,named]) " ^
1.106 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.107 " in [Q__Q, M__M, N__N, B__B])"),
1.108 - prep_met @{theory} "met_biege_setzrand" [] e_metID
1.109 + Specify.prep_met @{theory} "met_biege_setzrand" [] e_metID
1.110 (["Biegelinien", "setzeRandbedingungenEin"],
1.111 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.112 ("#Find" , ["Gleichungen equs'''"])],
1.113 @@ -414,7 +414,7 @@
1.114 " [Equation,fromFunction]) " ^
1.115 " [BOOL (hd f_s), BOOL b_4]) " ^
1.116 " in [e_1,e_2,e_3,e_4])"*)),
1.117 - prep_met @{theory} "met_equ_fromfun" [] e_metID
1.118 + Specify.prep_met @{theory} "met_equ_fromfun" [] e_metID
1.119 (["Equation","fromFunction"],
1.120 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.121 ("#Find" ,["equality equ'''"])],