equal
deleted
inserted
replaced
2835 context valid_trace |
2835 context valid_trace |
2836 begin |
2836 begin |
2837 |
2837 |
2838 lemma rtree_RAG: "rtree (RAG s)" |
2838 lemma rtree_RAG: "rtree (RAG s)" |
2839 using sgv_RAG acyclic_RAG |
2839 using sgv_RAG acyclic_RAG |
2840 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
2840 by (unfold rtree_def, auto) |
2841 |
2841 |
2842 end |
2842 end |
2843 |
2843 |
2844 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2844 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2845 using rtree_RAG . |
2845 using rtree_RAG . |