1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -185,9 +185,9 @@
1.4 Calc("op +", eval_binop "#add_")
1.5 ],
1.6 srls = Erls, calc = [],
1.7 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.8 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
1.9 Calc("op +", eval_binop "#add_"),
1.10 - Thm ("nth_Nil_",num_str nth_Nil_),
1.11 + Thm ("nth_Nil_",num_str @{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 @@ -206,19 +206,19 @@
1.16 Calc("op +", eval_binop "#add_")
1.17 ],
1.18 srls = Erls, calc = [],
1.19 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.20 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
1.21 Calc("op +", eval_binop "#add_"),
1.22 - Thm ("nth_Nil_", num_str nth_Nil_),
1.23 + Thm ("nth_Nil_", num_str @{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 filter_Cons),
1.30 - Thm ("filter_Nil", num_str filter_Nil),
1.31 - Thm ("if_True", num_str if_True),
1.32 - Thm ("if_False", num_str if_False),
1.33 - Thm ("hd_thm", num_str hd_thm)
1.34 + Thm ("filter_Cons", num_str @{filter_Cons),
1.35 + Thm ("filter_Nil", num_str @{filter_Nil),
1.36 + Thm ("if_True", num_str @{if_True),
1.37 + Thm ("if_False", num_str @{if_False),
1.38 + Thm ("hd_thm", num_str @{hd_thm)
1.39 ],
1.40 scr = EmptyScr};
1.41
1.42 @@ -235,8 +235,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 not_true),
1.47 - Thm ("not_false",num_str not_false)],
1.48 + Thm ("not_true",num_str @{not_true),
1.49 + Thm ("not_false",num_str @{not_false)],
1.50 calc = [], srls = srls, prls = Erls,
1.51 crls = Atools_erls, nrls = Erls},
1.52 "Script BiegelinieScript " ^
1.53 @@ -312,15 +312,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 not_true),
1.58 - Thm ("not_false",num_str not_false)],
1.59 + Thm ("not_true",num_str @{not_true),
1.60 + Thm ("not_false",num_str @{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 last_thmI),
1.66 - Thm ("if_True",num_str if_True),
1.67 - Thm ("if_False",num_str if_False)
1.68 + Thm ("last_thmI",num_str @{last_thmI),
1.69 + Thm ("if_True",num_str @{if_True),
1.70 + Thm ("if_False",num_str @{if_False)
1.71 ],
1.72 prls = Erls, crls = Atools_erls, nrls = Erls},
1.73 "Script Biegelinie2Script " ^
1.74 @@ -395,8 +395,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 not_true),
1.79 - Thm ("not_false",num_str not_false)],
1.80 + Thm ("not_true",num_str @{not_true),
1.81 + Thm ("not_false",num_str @{not_false)],
1.82 calc = [],
1.83 srls = append_rls "srls_ausBelastung" e_rls
1.84 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],