--- a/Implementation.thy	Wed Feb 03 12:04:03 2016 +0800
+++ b/Implementation.thy	Wed Feb 03 21:05:15 2016 +0800
@@ -376,9 +376,6 @@
 context valid_trace_p_w
 begin
 
-interpretation vat_e: valid_trace "e#s"
-  by (unfold_locales, insert vt_e, simp)
-
 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
   using holding_s_holder
   by (unfold s_RAG_def, fold holding_eq, auto)
@@ -428,13 +425,13 @@
   and "y \<in> ancestors (tRAG (e#s)) u"
   shows "cp_gen (e#s) y = cp_gen s y"
   using assms(3)
-proof(induct rule:wf_induct[OF vat_e.fsbttRAGs.wf])
+proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf])
   case (1 x)
   show ?case (is "?L = ?R")
   proof -
     from tRAG_ancestorsE[OF 1(2)]
     obtain th2 where eq_x: "x = Th th2" by blast
-    from vat_e.cp_gen_rec[OF this]
+    from vat_es.cp_gen_rec[OF this]
     have "?L = 
           Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" .
     also have "... = 
@@ -454,15 +451,15 @@
             assume "x \<in> Range {(Th th, Th holder)}"
             hence eq_x: "x = Th holder" using RangeE by auto
             show False
-            proof(cases rule:vat_e.ancestors_headE[OF assms(1) start])
+            proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
               case 1
-              from x_u[folded this, unfolded eq_x] vat_e.acyclic_tRAG
+              from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
               show ?thesis by (auto simp:ancestors_def acyclic_def)
             next
               case 2
               with x_u[unfolded eq_x]
               have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)
-              with vat_e.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
+              with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
             qed
           qed
         qed
@@ -473,7 +470,7 @@
           assume a_in: "a \<in> ?A"
           from 1(2)
           show "?f a = ?g a"
-          proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+          proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
              case in_ch
              show ?thesis
              proof(cases "a = u")
@@ -485,7 +482,7 @@
                 proof
                   assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                   have "a = u"
-                  proof(rule vat_e.rtree_s.ancestors_children_unique)
+                  proof(rule vat_es.rtree_s.ancestors_children_unique)
                     from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
                                           RTree.children (tRAG (e#s)) x" by auto
                   next 
@@ -519,7 +516,7 @@
               proof
                 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                 have "a = z"
-                proof(rule vat_e.rtree_s.ancestors_children_unique)
+                proof(rule vat_es.rtree_s.ancestors_children_unique)
                   from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
                       by (auto simp:ancestors_def)
                   with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
@@ -570,9 +567,6 @@
 context valid_trace_create
 begin 
 
-interpretation vat_e: valid_trace "e#s"
-  by (unfold_locales, insert vt_e, simp)
-
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
   by (unfold tRAG_alt_def RAG_unchanged, auto)
 
@@ -632,7 +626,7 @@
 qed
 
 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
- by (unfold vat_e.cp_rec children_of_th, simp add:the_preced_def)
+ by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
 
 end
 
@@ -706,4 +700,3 @@
 
 end
 
-