1253 (#1 (some_spec ospec spec), oris, []:I_Model.T, |
1253 (#1 (some_spec ospec spec), oris, []:I_Model.T, |
1254 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); |
1254 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); |
1255 val iii = appl_adds dI oris ppc pbt (selct::ss); |
1255 val iii = appl_adds dI oris ppc pbt (selct::ss); |
1256 tracing(I_Model.to_string thy iii); |
1256 tracing(I_Model.to_string thy iii); |
1257 |
1257 |
1258 val itm = appl_add' dI oris ppc pbt selct; |
1258 val itm = add_single' dI oris ppc pbt selct; |
1259 val ppc = insert_ppc' itm ppc; |
1259 val ppc = insert_ppc' itm ppc; |
1260 |
1260 |
1261 val _::selct::ss = (selct::ss); |
1261 val _::selct::ss = (selct::ss); |
1262 val itm = appl_add' dI oris ppc pbt selct; |
1262 val itm = add_single' dI oris ppc pbt selct; |
1263 val ppc = insert_ppc' itm ppc; |
1263 val ppc = insert_ppc' itm ppc; |
1264 |
1264 |
1265 val _::selct::ss = (selct::ss); |
1265 val _::selct::ss = (selct::ss); |
1266 val itm = appl_add' dI oris ppc pbt selct; |
1266 val itm = add_single' dI oris ppc pbt selct; |
1267 val ppc = insert_ppc' itm ppc; |
1267 val ppc = insert_ppc' itm ppc; |
1268 tracing(I_Model.to_string thy ppc); |
1268 tracing(I_Model.to_string thy ppc); |
1269 |
1269 |
1270 val _::selct::ss = (selct::ss); |
1270 val _::selct::ss = (selct::ss); |
1271 val itm = appl_add' dI oris ppc pbt selct; |
1271 val itm = add_single' dI oris ppc pbt selct; |
1272 val ppc = insert_ppc' itm ppc; |
1272 val ppc = insert_ppc' itm ppc; |
1273 *) |
1273 *) |
1274 "--------- fun concat_deriv --------------------------------------"; |
1274 "--------- fun concat_deriv --------------------------------------"; |
1275 "--------- fun concat_deriv --------------------------------------"; |
1275 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |