From 834d6a80773b29dc24bd5c84d26422ee9fb5d43f Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Fri, 14 Jun 2019 18:09:56 +0100 Subject: [PATCH] Updated for Isabelle2019. --- Core_DOM/monads/CharacterDataMonad.thy | 2 +- Core_DOM/monads/DocumentMonad.thy | 2 +- Core_DOM/monads/ElementMonad.thy | 2 +- Core_DOM/monads/NodeMonad.thy | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Core_DOM/monads/CharacterDataMonad.thy b/Core_DOM/monads/CharacterDataMonad.thy index 4506a2a..4e84b4f 100644 --- a/Core_DOM/monads/CharacterDataMonad.thy +++ b/Core_DOM/monads/CharacterDataMonad.thy @@ -59,7 +59,7 @@ lemma character_data_ptr_kinds_M_reads: using node_ptr_kinds_M_reads apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs character_data_ptr_kinds_def preserved_def) - by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def) + by (smt node_ptr_kinds_small preserved_def unit_all_impI) global_interpretation l_dummy defines get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a = "l_get_M.a_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a type_wf character_data_ptr_kinds" diff --git a/Core_DOM/monads/DocumentMonad.thy b/Core_DOM/monads/DocumentMonad.thy index 3ed400d..695f39d 100644 --- a/Core_DOM/monads/DocumentMonad.thy +++ b/Core_DOM/monads/DocumentMonad.thy @@ -58,7 +58,7 @@ lemma document_ptr_kinds_M_reads: apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs document_ptr_kinds_def preserved_def) - by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def) + by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI) global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds" diff --git a/Core_DOM/monads/ElementMonad.thy b/Core_DOM/monads/ElementMonad.thy index 89d028c..72870f7 100644 --- a/Core_DOM/monads/ElementMonad.thy +++ b/Core_DOM/monads/ElementMonad.thy @@ -56,7 +56,7 @@ lemma element_ptr_kinds_M_reads: "reads (\element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'" apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def node_ptr_kinds_M_reads preserved_def) - by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def) + by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI) global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds" diff --git a/Core_DOM/monads/NodeMonad.thy b/Core_DOM/monads/NodeMonad.thy index 91a9791..f915f54 100644 --- a/Core_DOM/monads/NodeMonad.thy +++ b/Core_DOM/monads/NodeMonad.thy @@ -77,7 +77,7 @@ lemma node_ptr_kinds_M_reads: using object_ptr_kinds_M_reads apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def object_ptr_kinds_M_reads preserved_def) - by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def) + by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI) global_interpretation l_put_M type_wf node_ptr_kinds get\<^sub>N\<^sub>o\<^sub>d\<^sub>e put\<^sub>N\<^sub>o\<^sub>d\<^sub>e rewrites "a_get_M = get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e"