equal
deleted
inserted
replaced
58 |
58 |
59 fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i; |
59 fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i; |
60 |
60 |
61 |
61 |
62 (*--------------------------------------------------------------- |
62 (*--------------------------------------------------------------- |
63 All in one -- not really needed. |
|
64 ---------------------------------------------------------------*) |
|
65 |
|
66 fun fuf_auto_tac css i = SOLVE (fuf_empty_tac css i) ORELSE TRY (fuf_tac css i); |
|
67 fun Fuf_auto_tac i = fuf_auto_tac (clasimpset ()) i; |
|
68 |
|
69 |
|
70 (*--------------------------------------------------------------- |
|
71 In fact could make this the only tactic: just need to |
63 In fact could make this the only tactic: just need to |
72 use contraposition and then look for empty set. |
64 use contraposition and then look for empty set. |
73 ---------------------------------------------------------------*) |
65 ---------------------------------------------------------------*) |
74 |
66 |
75 fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i; |
67 fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i; |