equal
deleted
inserted
replaced
44 qed "wf_asym"; |
44 qed "wf_asym"; |
45 |
45 |
46 val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; |
46 val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; |
47 by (rtac wf_asym 1); |
47 by (rtac wf_asym 1); |
48 by (REPEAT (resolve_tac prems 1)); |
48 by (REPEAT (resolve_tac prems 1)); |
49 qed "wf_anti_refl"; |
49 qed "wf_irrefl"; |
50 |
50 |
51 (*transitive closure of a wf relation is wf! *) |
51 (*transitive closure of a wf relation is wf! *) |
52 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
52 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
53 by (rewtac wf_def); |
53 by (rewtac wf_def); |
54 by (strip_tac 1); |
54 by (strip_tac 1); |