equal
deleted
inserted
replaced
233 |
233 |
234 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; |
234 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; |
235 by (simp_tac (simpset() addsimps [trancl_converse]) 1); |
235 by (simp_tac (simpset() addsimps [trancl_converse]) 1); |
236 qed "acyclic_converse"; |
236 qed "acyclic_converse"; |
237 |
237 |
|
238 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r"; |
|
239 by(blast_tac (claset() addIs [trancl_mono]) 1); |
|
240 qed "acyclic_subset"; |
|
241 |
238 (** cut **) |
242 (** cut **) |
239 |
243 |
240 (*This rewrite rule works upon formulae; thus it requires explicit use of |
244 (*This rewrite rule works upon formulae; thus it requires explicit use of |
241 H_cong to expose the equality*) |
245 H_cong to expose the equality*) |
242 Goalw [cut_def] |
246 Goalw [cut_def] |