1302 ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE a), (snd (Thm.dest_abs NONE b))) *} |
1302 ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE a), (snd (Thm.dest_abs NONE b))) *} |
1303 ML_prf {* val (a, b) = (snd (Thm.dest_comb a), snd (Thm.dest_comb b)) *} |
1303 ML_prf {* val (a, b) = (snd (Thm.dest_comb a), snd (Thm.dest_comb b)) *} |
1304 ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *} |
1304 ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *} |
1305 ML_prf {* (term_of a, term_of b) *} |
1305 ML_prf {* (term_of a, term_of b) *} |
1306 ML_prf {* (Envir.beta_norm (term_of a), term_of b) *} |
1306 ML_prf {* (Envir.beta_norm (term_of a), term_of b) *} |
1307 ML_prf {* Thm.beta_conv *} |
1307 ML_prf {* val man_inst_norm_r = Drule.beta_eta_conversion (cprop_of man_inst) *} |
1308 ML_prf man_inst |
1308 ML_prf {* val man_inst_norm = MetaSimplifier.rewrite_rule [man_inst_norm_r] man_inst *} |
1309 thm APPLY_RSP_I2 |
1309 ML_prf {* |
1310 apply (tactic {* compose_tac (false,man_inst,0) 1 *}) |
1310 val (tc') = (Logic.strip_assums_concl (prop_of man_inst_norm)); |
|
1311 val ps = Logic.strip_params (prop_of man_inst_norm) |
|
1312 val tt = Term.list_abs (ps, tc') |
|
1313 val ct = cterm_of @{theory} tt |
|
1314 *} |
|
1315 ML_prf {* Thm.match (ct, goal') *} |
|
1316 ML_prf {* PRIMSEQ *} |
|
1317 ML_prf {* man_inst_norm *} |
|
1318 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *}) |
|
1319 |
|
1320 |
|
1321 |
1311 |
1322 |
1312 sorry |
1323 sorry |
1313 |
1324 |
1314 thm list.recs(2) |
1325 thm list.recs(2) |
1315 |
1326 |