diff --git a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy
index 55e2271..55873ed 100644
--- a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy
@@ -4239,7 +4239,7 @@ locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\
   l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
 begin
 
-lemma adopt_node_removes_child:
+lemma adopt_node_removes_child_step:
   assumes wellformed: "heap_is_wellformed h"
     and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2"
     and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@@ -4286,12 +4286,12 @@ proof -
   qed
 qed
 
-lemma adopt_node_removes_child_thesis:
+lemma adopt_node_removes_child:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
 shows "\<And>ptr' children'.
   h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'"
-  using adopt_node_removes_child assms by blast
+  using adopt_node_removes_child_step assms by blast
 
 lemma adopt_node_preserves_wellformedness:
   assumes "heap_is_wellformed h"
@@ -5035,7 +5035,7 @@ locale l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
   l_get_owner_document_wf
 begin
 
-lemma insert_before_preserves_acyclitity_thesis:
+lemma insert_before_preserves_acyclitity:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
 shows "acyclic (parent_child_rel h')"
@@ -5736,7 +5736,7 @@ proof -
     by (simp add: heap_is_wellformed_def)
 qed
 
-lemma adopt_node_children_remain_distinct_thesis:
+lemma adopt_node_children_remain_distinct:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
 shows "\<And>ptr' children'.
@@ -5745,7 +5745,7 @@ shows "\<And>ptr' children'.
   by blast
 
 
-lemma insert_node_children_remain_distinct_thesis:
+lemma insert_node_children_remain_distinct:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> a_insert_node ptr new_child reference_child_opt \<rightarrow>\<^sub>h h'"
   assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@@ -5768,7 +5768,7 @@ proof -
     using assms(5) assms(6) insert_before_list_distinct returns_result_eq by fastforce
 qed
 
-lemma insert_before_children_remain_distinct_thesis:
+lemma insert_before_children_remain_distinct:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> insert_before ptr new_child child_opt \<rightarrow>\<^sub>h h'"
 shows "\<And>ptr' children'.
@@ -5795,7 +5795,7 @@ proof -
 
   have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
       \<Longrightarrow> distinct children"
-    using adopt_node_children_remain_distinct_thesis
+    using adopt_node_children_remain_distinct
     using assms(1) assms(2) assms(3) h2
     by blast
   moreover have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
@@ -5814,7 +5814,7 @@ proof -
 qed
 
 
-lemma insert_before_removes_child_thesis:
+lemma insert_before_removes_child:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
   assumes "ptr \<noteq> ptr'"
diff --git a/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy b/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
index 7c16c10..e674f14 100644
--- a/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
@@ -4242,7 +4242,7 @@ locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\
   l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
 begin
 
-lemma adopt_node_removes_child:
+lemma adopt_node_removes_child_step:
   assumes wellformed: "heap_is_wellformed h"
     and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2"
     and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@@ -4289,12 +4289,12 @@ proof -
   qed
 qed
 
-lemma adopt_node_removes_child_thesis:
+lemma adopt_node_removes_child:
   assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
   assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
 shows "\<And>ptr' children'.
   h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'"
-  using adopt_node_removes_child assms by blast
+  using adopt_node_removes_child_step assms by blast
 
 lemma adopt_node_preserves_wellformedness:
   assumes "heap_is_wellformed h"