diff --git a/Core_DOM/classes/CharacterDataClass.thy b/Core_DOM/classes/CharacterDataClass.thy index cf0ee61..cf9786f 100644 --- a/Core_DOM/classes/CharacterDataClass.thy +++ b/Core_DOM/classes/CharacterDataClass.thy @@ -64,7 +64,8 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume = "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'CharacterData option RCharacterData_ext + 'Node, 'Element) heap" register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, - 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap" + 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap" +type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" definition character_data_ptr_kinds :: "(_) heap \ (_) character_data_ptr fset" diff --git a/Core_DOM/classes/DocumentClass.thy b/Core_DOM/classes/DocumentClass.thy index 84a1990..0cc7880 100644 --- a/Core_DOM/classes/DocumentClass.thy +++ b/Core_DOM/classes/DocumentClass.thy @@ -64,7 +64,8 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume 'Element, 'CharacterData) heap" register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, - 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap" + 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap" +type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" definition document_ptr_kinds :: "(_) heap \ (_) document_ptr fset" diff --git a/Core_DOM/classes/ElementClass.thy b/Core_DOM/classes/ElementClass.thy index d7f624d..dd647a5 100644 --- a/Core_DOM/classes/ElementClass.thy +++ b/Core_DOM/classes/ElementClass.thy @@ -68,6 +68,7 @@ type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) heap" register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) heap" +type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" definition element_ptr_kinds :: "(_) heap \ (_) element_ptr fset" where diff --git a/Core_DOM/classes/NodeClass.thy b/Core_DOM/classes/NodeClass.thy index 5670183..fdbbff1 100644 --- a/Core_DOM/classes/NodeClass.thy +++ b/Core_DOM/classes/NodeClass.thy @@ -51,6 +51,7 @@ type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node) heap = "('node_ptr node_ptr + 'object_ptr, 'Node RNode_ext + 'Object) heap" register_default_tvars "('object_ptr, 'node_ptr, 'Object, 'Node) heap" +type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit) heap" definition node_ptr_kinds :: "(_) heap \ (_) node_ptr fset" diff --git a/Core_DOM/classes/ObjectClass.thy b/Core_DOM/classes/ObjectClass.thy index d7cbeb9..b3091ef 100644 --- a/Core_DOM/classes/ObjectClass.thy +++ b/Core_DOM/classes/ObjectClass.thy @@ -44,7 +44,8 @@ type_synonym 'Object Object = "'Object RObject_scheme" register_default_tvars "'Object Object" datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap") -register_default_tvars "('object_ptr, 'Object) heap" +register_default_tvars "('object_ptr, 'Object) heap" +type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap" definition object_ptr_kinds :: "(_) heap \ (_) object_ptr fset" where diff --git a/Core_DOM/tests/Document_adoptNode.thy b/Core_DOM/tests/Document_adoptNode.thy index 4adb19b..3135aa5 100644 --- a/Core_DOM/tests/Document_adoptNode.thy +++ b/Core_DOM/tests/Document_adoptNode.thy @@ -35,7 +35,7 @@ imports "Core_DOM_BaseTest" begin -definition Document_adoptNode_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where +definition Document_adoptNode_heap :: heap⇩f⇩i⇩n⇩a⇩l where "Document_adoptNode_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])), (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 8)] fmempty None)), (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7)] fmempty None)), diff --git a/Core_DOM/tests/Document_getElementById.thy b/Core_DOM/tests/Document_getElementById.thy index 9ece29a..f816d05 100644 --- a/Core_DOM/tests/Document_getElementById.thy +++ b/Core_DOM/tests/Document_getElementById.thy @@ -35,7 +35,7 @@ imports "Core_DOM_BaseTest" begin -definition Document_getElementById_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where +definition Document_getElementById_heap :: heap⇩f⇩i⇩n⇩a⇩l where "Document_getElementById_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])), (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 9)] fmempty None)), (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7), cast (element_ptr.Ref 8)] fmempty None)), diff --git a/Core_DOM/tests/Node_insertBefore.thy b/Core_DOM/tests/Node_insertBefore.thy index 48d1b19..64284cb 100644 --- a/Core_DOM/tests/Node_insertBefore.thy +++ b/Core_DOM/tests/Node_insertBefore.thy @@ -35,7 +35,7 @@ imports "Core_DOM_BaseTest" begin -definition Node_insertBefore_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where +definition Node_insertBefore_heap :: heap⇩f⇩i⇩n⇩a⇩l where "Node_insertBefore_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])), (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 6)] fmempty None)), (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5)] fmempty None)), diff --git a/Core_DOM/tests/Node_removeChild.thy b/Core_DOM/tests/Node_removeChild.thy index 74dfa2c..812db93 100644 --- a/Core_DOM/tests/Node_removeChild.thy +++ b/Core_DOM/tests/Node_removeChild.thy @@ -35,7 +35,7 @@ imports "Core_DOM_BaseTest" begin -definition Node_removeChild_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where +definition Node_removeChild_heap :: heap⇩f⇩i⇩n⇩a⇩l where "Node_removeChild_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])), (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 7)] fmempty None)), (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6)] fmempty None)),