1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Feb 25 16:31:17 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Fri Mar 02 14:19:59 2018 +0100
1.3 @@ -146,9 +146,9 @@
1.4 Calc("Groups.plus_class.plus", eval_binop "#add_")
1.5 ],
1.6 srls = Erls, calc = [], errpatts = [],
1.7 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.8 + rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.9 Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.10 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.11 + Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.12 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.13 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.14 Calc("Atools.argument'_in",
1.15 @@ -167,19 +167,19 @@
1.16 Calc("Groups.plus_class.plus", eval_binop "#add_")
1.17 ],
1.18 srls = Erls, calc = [], errpatts = [],
1.19 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.20 + rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.21 Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.22 - Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
1.23 + Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
1.24 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.25 Calc("Atools.filter'_sameFunId",
1.26 eval_filter_sameFunId "Atools.filter'_sameFunId"),
1.27 (*WN070514 just for smltest/../biegelinie.sml ...*)
1.28 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
1.29 - Thm ("filter_Cons", num_str @{thm filter_Cons}),
1.30 - Thm ("filter_Nil", num_str @{thm filter_Nil}),
1.31 - Thm ("if_True", num_str @{thm if_True}),
1.32 - Thm ("if_False", num_str @{thm if_False}),
1.33 - Thm ("hd_thm", num_str @{thm hd_thm})
1.34 + Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}),
1.35 + Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}),
1.36 + Thm ("if_True", TermC.num_str @{thm if_True}),
1.37 + Thm ("if_False", TermC.num_str @{thm if_False}),
1.38 + Thm ("hd_thm", TermC.num_str @{thm hd_thm})
1.39 ],
1.40 scr = EmptyScr};
1.41 *}
1.42 @@ -194,8 +194,8 @@
1.43 {rew_ord'="tless_true",
1.44 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.45 [Calc ("Atools.ident",eval_ident "#ident_"),
1.46 - Thm ("not_true",num_str @{thm not_true}),
1.47 - Thm ("not_false",num_str @{thm not_false})],
1.48 + Thm ("not_true",TermC.num_str @{thm not_true}),
1.49 + Thm ("not_false",TermC.num_str @{thm not_false})],
1.50 calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
1.51 "Script BiegelinieScript " ^
1.52 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.53 @@ -270,15 +270,15 @@
1.54 {rew_ord'="tless_true",
1.55 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.56 [Calc ("Atools.ident",eval_ident "#ident_"),
1.57 - Thm ("not_true",num_str @{thm not_true}),
1.58 - Thm ("not_false",num_str @{thm not_false})],
1.59 + Thm ("not_true",TermC.num_str @{thm not_true}),
1.60 + Thm ("not_false",TermC.num_str @{thm not_false})],
1.61 calc = [],
1.62 srls = append_rls "erls_IntegrierenUndK.." e_rls
1.63 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.64 Calc ("Atools.ident",eval_ident "#ident_"),
1.65 - Thm ("last_thmI",num_str @{thm last_thmI}),
1.66 - Thm ("if_True",num_str @{thm if_True}),
1.67 - Thm ("if_False",num_str @{thm if_False})],
1.68 + Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
1.69 + Thm ("if_True",TermC.num_str @{thm if_True}),
1.70 + Thm ("if_False",TermC.num_str @{thm if_False})],
1.71 prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
1.72 "Script Biegelinie2Script " ^
1.73 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.74 @@ -325,8 +325,8 @@
1.75 {rew_ord'="tless_true",
1.76 rls' = append_rls "erls_ausBelastung" e_rls
1.77 [Calc ("Atools.ident", eval_ident "#ident_"),
1.78 - Thm ("not_true", num_str @{thm not_true}),
1.79 - Thm ("not_false", num_str @{thm not_false})],
1.80 + Thm ("not_true", TermC.num_str @{thm not_true}),
1.81 + Thm ("not_false", TermC.num_str @{thm not_false})],
1.82 calc = [],
1.83 srls = append_rls "srls_ausBelastung" e_rls
1.84 [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],