From 86ea8d481731442c564e44c70b5ef6ca189a18cf Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 16 Apr 2020 23:58:58 +0100 Subject: [PATCH] Restrict auto. --- Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 e0362fa..7c16c10 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 @@ -3041,7 +3041,7 @@ proof - assume "is_node_ptr_kind ptr" then have ?thesis using \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ - apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def) + apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)[1] apply(split invoke_splits, (rule conjI | rule impI)+)+ apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl]) apply(drule(1) known_ptr_not_character_data_ptr)