equal
deleted
inserted
replaced
128 by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
128 by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
129 qed "wf_insert"; |
129 qed "wf_insert"; |
130 AddIffs [wf_insert]; |
130 AddIffs [wf_insert]; |
131 |
131 |
132 (*** acyclic ***) |
132 (*** acyclic ***) |
|
133 |
|
134 val acyclicI = prove_goalw WF.thy [acyclic_def] |
|
135 "!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]); |
133 |
136 |
134 goalw WF.thy [acyclic_def] |
137 goalw WF.thy [acyclic_def] |
135 "!!r. wf r ==> acyclic r"; |
138 "!!r. wf r ==> acyclic r"; |
136 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); |
139 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); |
137 qed "wf_acyclic"; |
140 qed "wf_acyclic"; |