equal
deleted
inserted
replaced
96 derive_chains ctxt chain_tac |
96 derive_chains ctxt chain_tac |
97 (decompose_tac' ctxt cont err_cont) |
97 (decompose_tac' ctxt cont err_cont) |
98 |
98 |
99 fun auto_decompose_tac ctxt = |
99 fun auto_decompose_tac ctxt = |
100 Termination.TERMINATION ctxt |
100 Termination.TERMINATION ctxt |
101 (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt)) |
101 (decompose_tac ctxt (auto_tac (clasimpset_of ctxt)) |
102 (K (K all_tac)) (K (K no_tac))) |
102 (K (K all_tac)) (K (K no_tac))) |
103 |
103 |
104 |
104 |
105 end |
105 end |