Renamed final_heap due to some weird isabelle build errors.

Core_DOM/classes/CharacterDataClass.thy

@@ -65,7 +65,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
       '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"   
-type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"
+type_synonym heap_final = "(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

@@ -65,7 +65,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
 register_default_tvars 
   "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 
   '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"
+type_synonym heap_final = "(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,7 +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"
+type_synonym heap_final = "(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,7 +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"
+type_synonym heap_final = "(unit, unit, unit, unit) heap"
 
 
 definition node_ptr_kinds :: "(_) heap \<Rightarrow> (_) node_ptr fset"

Core_DOM/classes/ObjectClass.thy

@@ -45,7 +45,7 @@ register_default_tvars "'Object Object"
 
 datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
 register_default_tvars "('object_ptr, 'Object) heap"
-type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap"
+type_synonym heap_final = "(unit, unit) heap"
 
 definition object_ptr_kinds :: "(_) heap \<Rightarrow> (_) object_ptr fset"
   where

Core_DOM/tests/Document_adoptNode.thy

@@ -29,15 +29,15 @@
 
 (* This file is automatically generated, please do not modify! *)
 
-section\<open>Testing Document_adoptNode\<close>
-text\<open>This theory contains the test cases for Document_adoptNode.\<close>
+section\<open>Testing Document\_adoptNode\<close>
+text\<open>This theory contains the test cases for Document\_adoptNode.\<close>
 
 theory Document_adoptNode
 imports
   "Core_DOM_BaseTest"
 begin
 
-definition Document_adoptNode_heap :: heap⇩f⇩i⇩n⇩a⇩l where
+definition Document_adoptNode_heap :: heap_final 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

@@ -29,15 +29,15 @@
 
 (* This file is automatically generated, please do not modify! *)
 
-section\<open>Testing Document_getElementById\<close>
-text\<open>This theory contains the test cases for Document_getElementById.\<close>
+section\<open>Testing Document\_getElementById\<close>
+text\<open>This theory contains the test cases for Document\_getElementById.\<close>
 
 theory Document_getElementById
 imports
   "Core_DOM_BaseTest"
 begin
 
-definition Document_getElementById_heap :: heap⇩f⇩i⇩n⇩a⇩l where
+definition Document_getElementById_heap :: heap_final 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

@@ -29,15 +29,15 @@
 
 (* This file is automatically generated, please do not modify! *)
 
-section\<open>Testing Node_insertBefore\<close>
-text\<open>This theory contains the test cases for Node_insertBefore.\<close>
+section\<open>Testing Node\_insertBefore\<close>
+text\<open>This theory contains the test cases for Node\_insertBefore.\<close>
 
 theory Node_insertBefore
 imports
   "Core_DOM_BaseTest"
 begin
 
-definition Node_insertBefore_heap :: heap⇩f⇩i⇩n⇩a⇩l where
+definition Node_insertBefore_heap :: heap_final 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

@@ -29,15 +29,15 @@
 
 (* This file is automatically generated, please do not modify! *)
 
-section\<open>Testing Node_removeChild\<close>
-text\<open>This theory contains the test cases for Node_removeChild.\<close>
+section\<open>Testing Node\_removeChild\<close>
+text\<open>This theory contains the test cases for Node\_removeChild.\<close>
 
 theory Node_removeChild
 imports
   "Core_DOM_BaseTest"
 begin
 
-definition Node_removeChild_heap :: heap⇩f⇩i⇩n⇩a⇩l where
+definition Node_removeChild_heap :: heap_final 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)),