Added heap_final shorthand.

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 \<Rightarrow> (_) character_data_ptr fset"

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 \<Rightarrow> (_) document_ptr fset"

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 \<Rightarrow> (_) element_ptr fset"
   where

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 \<Rightarrow> (_) node_ptr fset"

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 \<Rightarrow> (_) object_ptr fset"
   where

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)),

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)),

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)),

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)),