equal
deleted
inserted
replaced
65 let |
65 let |
66 fun tac [] st = all_tac st |
66 fun tac [] st = all_tac st |
67 | tac (type_enc :: type_encs) st = |
67 | tac (type_enc :: type_encs) st = |
68 st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |
68 st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |
69 |> ((if null type_encs then all_tac else rtac @{thm fork} 1) |
69 |> ((if null type_encs then all_tac else rtac @{thm fork} 1) |
70 THEN Metis_Tactic.metis_tac [type_enc] "combinators" ctxt ths 1 |
70 THEN Metis_Tactic.metis_tac [type_enc] |
|
71 ATP_Problem_Generate.combsN ctxt ths 1 |
71 THEN COND (has_fewer_prems 2) all_tac no_tac |
72 THEN COND (has_fewer_prems 2) all_tac no_tac |
72 THEN tac type_encs) |
73 THEN tac type_encs) |
73 in tac end |
74 in tac end |
74 *} |
75 *} |
75 |
76 |