diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile
index 6b45e45..ff7a320 100644
--- a/.ci/Jenkinsfile
+++ b/.ci/Jenkinsfile
@@ -3,7 +3,7 @@ pipeline {
     stages {
         stage('Build') {
             steps {
-                sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2018 isabelle build -D /Core_DOM'
+                sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2019 isabelle build -D /Core_DOM'
             }
         }
     }
diff --git a/Core_DOM/ROOT b/Core_DOM/ROOT
index 798cf8e..414b196 100644
--- a/Core_DOM/ROOT
+++ b/Core_DOM/ROOT
@@ -1,7 +1,7 @@
 chapter AFP
 
 session "Core_DOM-devel" (AFP) = "HOL-Library" + 
-  options [timeout = 600] 
+  options [timeout = 1200] 
   theories
     Core_DOM
     Core_DOM_Tests
diff --git a/Core_DOM/monads/CharacterDataMonad.thy b/Core_DOM/monads/CharacterDataMonad.thy
index 4506a2a..9811731 100644
--- a/Core_DOM/monads/CharacterDataMonad.thy
+++ b/Core_DOM/monads/CharacterDataMonad.thy
@@ -57,9 +57,10 @@ lemma character_data_ptr_kinds_M_eq:
 lemma character_data_ptr_kinds_M_reads: 
   "reads (\<Union>node_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node_ptr RObject.nothing)}) character_data_ptr_kinds_M h h'"
   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)
+  apply (simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs 
+    character_data_ptr_kinds_def preserved_def cong del: image_cong_simp)
+  apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
+  done
 
 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..d2d17a5 100644
--- a/Core_DOM/monads/DocumentMonad.thy
+++ b/Core_DOM/monads/DocumentMonad.thy
@@ -55,10 +55,10 @@ lemma document_ptr_kinds_M_eq:
 lemma document_ptr_kinds_M_reads: 
   "reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) document_ptr_kinds_M h h'"
   using object_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)
+  apply (simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs 
+    document_ptr_kinds_def preserved_def cong del: image_cong_simp)
+  apply (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
+  done
 
 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..59fcc71 100644
--- a/Core_DOM/monads/ElementMonad.thy
+++ b/Core_DOM/monads/ElementMonad.thy
@@ -54,9 +54,10 @@ lemma element_ptr_kinds_M_eq:
 
 lemma element_ptr_kinds_M_reads: 
   "reads (\<Union>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)
+  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 cong del: image_cong_simp)
+  apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
+  done
 
 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..b669f1d 100644
--- a/Core_DOM/monads/NodeMonad.thy
+++ b/Core_DOM/monads/NodeMonad.thy
@@ -75,9 +75,10 @@ global_interpretation l_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf by
 lemma node_ptr_kinds_M_reads: 
   "reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
   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)
+  apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
+    object_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
+  apply (metis (mono_tags, hide_lams)  object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
+  done
 
 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" 
diff --git a/Core_DOM/tests/Document-adoptNode.html.orig b/Core_DOM/tests/Document-adoptNode.html.orig
deleted file mode 100644
index 584d5d9..0000000
--- a/Core_DOM/tests/Document-adoptNode.html.orig
+++ /dev/null
@@ -1,50 +0,0 @@
-<!doctype html>
-<meta charset=utf-8>
-<title>Document.adoptNode</title>
-<link rel=help href="https://dom.spec.whatwg.org/#dom-document-adoptnode">
-<script src="/resources/testharness.js"></script>
-<script src="/resources/testharnessreport.js"></script>
-<div id="log"></div>
-<!--creates an element with local name "x<": --><x<>x</x<>
-<script>
-test(function() {
-  var y = document.getElementsByTagName("x<")[0]
-  var child = y.firstChild
-  assert_equals(y.parentNode, document.body)
-  assert_equals(y.ownerDocument, document)
-  assert_equals(document.adoptNode(y), y)
-  assert_equals(y.parentNode, null)
-  assert_equals(y.firstChild, child)
-  assert_equals(y.ownerDocument, document)
-  assert_equals(child.ownerDocument, document)
-  var doc = document.implementation.createDocument(null, null, null)
-  assert_equals(doc.adoptNode(y), y)
-  assert_equals(y.parentNode, null)
-  assert_equals(y.firstChild, child)
-  assert_equals(y.ownerDocument, doc)
-  assert_equals(child.ownerDocument, doc)
-}, "Adopting an Element called 'x<' should work.")
-
-test(function() {
-  var x = document.createElement(":good:times:")
-  assert_equals(document.adoptNode(x), x);
-  var doc = document.implementation.createDocument(null, null, null)
-  assert_equals(doc.adoptNode(x), x)
-  assert_equals(x.parentNode, null)
-  assert_equals(x.ownerDocument, doc)
-}, "Adopting an Element called ':good:times:' should work.")
-
-test(function() {
-  var doctype = document.doctype;
-  assert_equals(doctype.parentNode, document)
-  assert_equals(doctype.ownerDocument, document)
-  assert_equals(document.adoptNode(doctype), doctype)
-  assert_equals(doctype.parentNode, null)
-  assert_equals(doctype.ownerDocument, document)
-}, "Explicitly adopting a DocumentType should work.")
-
-test(function() {
-  var doc = document.implementation.createDocument(null, null, null)
-  assert_throws("NOT_SUPPORTED_ERR", function() { document.adoptNode(doc) })
-}, "Adopting a Document should throw.")
-</script>
diff --git a/Core_DOM/tests/Document-getElementById.html.orig b/Core_DOM/tests/Document-getElementById.html.orig
deleted file mode 100644
index 1dec4c0..0000000
--- a/Core_DOM/tests/Document-getElementById.html.orig
+++ /dev/null
@@ -1,350 +0,0 @@
-<!DOCTYPE html>
-<meta charset=utf-8>
-<title>Document.getElementById</title>
-<link rel="author" title="Tetsuharu OHZEKI" href="mailto:saneyuki.snyk@gmail.com">
-<link rel=help href="https://dom.spec.whatwg.org/#dom-document-getelementbyid">
-<script src="/resources/testharness.js"></script>
-<script src="/resources/testharnessreport.js"></script>
-<body>
-  <div id="log"></div>
-
-  <!-- test 0 -->
-  <div id=""></div>
-
-  <!-- test 1 -->
-  <div id="test1"></div>
-
-  <!-- test 5 -->
-  <div id="test5" data-name="1st">
-    <p id="test5" data-name="2nd">P</p>
-    <input id="test5" type="submit" value="Submit" data-name="3rd">
-  </div>
-
-  <!-- test 15 -->
-  <div id="outer">
-    <div id="middle">
-      <div id="inner"></div>
-    </div>
-  </div>
-
-<script>
-  var gBody = document.getElementsByTagName("body")[0];
-
-  test(function() {
-    assert_equals(document.getElementById(""), null);
-  }, "Calling document.getElementById with an empty string argument.");
-
-  test(function() {
-    var element = document.createElement("div");
-    element.setAttribute("id", "null");
-    document.body.appendChild(element);
-    this.add_cleanup(function() { document.body.removeChild(element) });
-    assert_equals(document.getElementById(null), element);
-  }, "Calling document.getElementById with a null argument.");
-
-  test(function() {
-    var element = document.createElement("div");
-    element.setAttribute("id", "undefined");
-    document.body.appendChild(element);
-    this.add_cleanup(function() { document.body.removeChild(element) });
-    assert_equals(document.getElementById(undefined), element);
-  }, "Calling document.getElementById with an undefined argument.");
-
-
-  test(function() {
-    var bar = document.getElementById("test1");
-    assert_not_equals(bar, null, "should not be null");
-    assert_equals(bar.tagName, "DIV", "should have expected tag name.");
-    assert_true(bar instanceof HTMLDivElement, "should be a valid Element instance");
-  }, "on static page");
-
-
-  test(function() {
-    var TEST_ID = "test2";
-
-    var test = document.createElement("div");
-    test.setAttribute("id", TEST_ID);
-    gBody.appendChild(test);
-
-    // test: appended element
-    var result = document.getElementById(TEST_ID);
-    assert_not_equals(result, null, "should not be null.");
-    assert_equals(result.tagName, "DIV", "should have appended element's tag name");
-    assert_true(result instanceof HTMLDivElement, "should be a valid Element instance");
-
-    // test: removed element
-    gBody.removeChild(test);
-    var removed = document.getElementById(TEST_ID);
-    // `document.getElementById()` returns `null` if there is none.
-    // https://dom.spec.whatwg.org/#dom-nonelementparentnode-getelementbyid
-    assert_equals(removed, null, "should not get removed element.");
-  }, "Document.getElementById with a script-inserted element");
-
-
-  test(function() {
-    // setup fixtures.
-    var TEST_ID = "test3";
-    var test = document.createElement("div");
-    test.setAttribute("id", TEST_ID);
-    gBody.appendChild(test);
-
-    // update id
-    var UPDATED_ID = "test3-updated";
-    test.setAttribute("id", UPDATED_ID);
-    var e = document.getElementById(UPDATED_ID);
-    assert_equals(e, test, "should get the element with id.");
-
-    var old = document.getElementById(TEST_ID);
-    assert_equals(old, null, "shouldn't get the element by the old id.");
-
-    // remove id.
-    test.removeAttribute("id");
-    var e2 = document.getElementById(UPDATED_ID);
-    assert_equals(e2, null, "should return null when the passed id is none in document.");
-  }, "update `id` attribute via setAttribute/removeAttribute");
-
-
-  test(function() {
-    var TEST_ID = "test4-should-not-exist";
-
-    var e = document.createElement('div');
-    e.setAttribute("id", TEST_ID);
-
-    assert_equals(document.getElementById(TEST_ID), null, "should be null");
-    document.body.appendChild(e);
-    assert_equals(document.getElementById(TEST_ID), e, "should be the appended element");
-  }, "Ensure that the id attribute only affects elements present in a document");
-
-
-  test(function() {
-    // the method should return the 1st element.
-    var TEST_ID = "test5";
-    var target = document.getElementById(TEST_ID);
-    assert_not_equals(target, null, "should not be null");
-    assert_equals(target.getAttribute("data-name"), "1st", "should return the 1st");
-
-    // even if after the new element was appended.
-    var element4 = document.createElement("div");
-    element4.setAttribute("id", TEST_ID);
-    element4.setAttribute("data-name", "4th");
-    gBody.appendChild(element4);
-    var target2 = document.getElementById(TEST_ID);
-    assert_not_equals(target2, null, "should not be null");
-    assert_equals(target2.getAttribute("data-name"), "1st", "should be the 1st");
-
-    // should return the next element after removed the subtree including the 1st element.
-    target2.parentNode.removeChild(target2);
-    var target3 = document.getElementById(TEST_ID);
-    assert_not_equals(target3, null, "should not be null");
-    assert_equals(target3.getAttribute("data-name"), "4th", "should be the 4th");
-  }, "in tree order, within the context object's tree");
-
-
-  test(function() {
-    var TEST_ID = "test6";
-    var s = document.createElement("div");
-    s.setAttribute("id", TEST_ID);
-    // append to Element, not Document.
-    document.createElement("div").appendChild(s);
-
-    assert_equals(document.getElementById(TEST_ID), null, "should be null");
-  }, "Modern browsers optimize this method with using internal id cache. " +
-     "This test checks that their optimization should effect only append to `Document`, not append to `Node`.");
-
-
-  test(function() {
-    var TEST_ID = "test7"
-    var element = document.createElement("div");
-    element.setAttribute("id", TEST_ID);
-    gBody.appendChild(element);
-
-    var target = document.getElementById(TEST_ID);
-    assert_equals(target, element, "should return the element before changing the value");
-
-    element.attributes[0].value = TEST_ID + "-updated";
-    var target2 = document.getElementById(TEST_ID);
-    assert_equals(target2, null, "should return null after updated id via Attr.value");
-    var target3 = document.getElementById(TEST_ID + "-updated");
-    assert_equals(target3, element, "should be equal to the updated element.");
-  }, "changing attribute's value via `Attr` gotten from `Element.attribute`.");
-
-
-  test(function() {
-    var TEST_ID = "test8";
-
-    // setup fixture
-    var element = document.createElement("div");
-    element.setAttribute("id", TEST_ID + "-fixture");
-    gBody.appendChild(element);
-
-    // add id-ed element with using innerHTML
-    element.innerHTML = "<div id='"+ TEST_ID +"'></div>";
-    var test = document.getElementById(TEST_ID);
-    assert_equals(test, element.firstChild, "should not be null");
-    assert_equals(test.tagName, "DIV", "should have expected tag name.");
-    assert_true(test instanceof HTMLDivElement, "should be a valid Element instance");
-  }, "add id attribute via innerHTML");
-
-
-  test(function() {
-    var TEST_ID = "test9";
-
-    // add fixture
-    var fixture = document.createElement("div");
-    fixture.setAttribute("id", TEST_ID + "-fixture");
-    gBody.appendChild(fixture);
-
-    var element = document.createElement("div");
-    element.setAttribute("id", TEST_ID);
-    fixture.appendChild(element);
-
-    // check 'getElementById' should get the 'element'
-    assert_equals(document.getElementById(TEST_ID), element, "should not be null");
-
-    // remove id-ed element with using innerHTML (clear 'element')
-    fixture.innerHTML = "";
-    var test = document.getElementById(TEST_ID);
-    assert_equals(test, null, "should be null.");
-  }, "remove id attribute via innerHTML");
-
-
-  test(function() {
-    var TEST_ID = "test10";
-
-    // setup fixture
-    var element = document.createElement("div");
-    element.setAttribute("id", TEST_ID + "-fixture");
-    gBody.appendChild(element);
-
-    // add id-ed element with using outerHTML
-    element.outerHTML = "<div id='"+ TEST_ID +"'></div>";
-    var test = document.getElementById(TEST_ID);
-    assert_not_equals(test, null, "should not be null");
-    assert_equals(test.tagName, "DIV", "should have expected tag name.");
-    assert_true(test instanceof HTMLDivElement,"should be a valid Element instance");
-  }, "add id attribute via outerHTML");
-
-
-  test(function() {
-    var TEST_ID = "test11";
-
-    var element = document.createElement("div");
-    element.setAttribute("id", TEST_ID);
-    gBody.appendChild(element);
-
-    var test = document.getElementById(TEST_ID);
-    assert_equals(test, element, "should be equal to the appended element.");
-
-    // remove id-ed element with using outerHTML
-    element.outerHTML = "<div></div>";
-    var test = document.getElementById(TEST_ID);
-    assert_equals(test, null, "should be null.");
-  }, "remove id attribute via outerHTML");
-
-
-  test(function() {
-    // setup fixtures.
-    var TEST_ID = "test12";
-    var test = document.createElement("div");
-    test.id = TEST_ID;
-    gBody.appendChild(test);
-
-    // update id
-    var UPDATED_ID = TEST_ID + "-updated";
-    test.id =  UPDATED_ID;
-    var e = document.getElementById(UPDATED_ID);
-    assert_equals(e, test, "should get the element with id.");
-
-    var old = document.getElementById(TEST_ID);
-    assert_equals(old, null, "shouldn't get the element by the old id.");
-
-    // remove id.
-    test.id = "";
-    var e2 = document.getElementById(UPDATED_ID);
-    assert_equals(e2, null, "should return null when the passed id is none in document.");
-  }, "update `id` attribute via element.id");
-
-
-  test(function() {
-    var TEST_ID = "test13";
-
-    var create_same_id_element = function (order) {
-      var element = document.createElement("div");
-      element.setAttribute("id", TEST_ID);
-      element.setAttribute("data-order", order);// for debug
-      return element;
-    };
-
-    // create fixture
-    var container = document.createElement("div");
-    container.setAttribute("id", TEST_ID + "-fixture");
-    gBody.appendChild(container);
-
-    var element1 = create_same_id_element("1");
-    var element2 = create_same_id_element("2");
-    var element3 = create_same_id_element("3");
-    var element4 = create_same_id_element("4");
-
-    // append element: 2 -> 4 -> 3 -> 1
-    container.appendChild(element2);
-    container.appendChild(element4);
-    container.insertBefore(element3, element4);
-    container.insertBefore(element1, element2);
-
-
-    var test = document.getElementById(TEST_ID);
-    assert_equals(test, element1, "should return 1st element");
-    container.removeChild(element1);
-
-    test = document.getElementById(TEST_ID);
-    assert_equals(test, element2, "should return 2nd element");
-    container.removeChild(element2);
-
-    test = document.getElementById(TEST_ID);
-    assert_equals(test, element3, "should return 3rd element");
-    container.removeChild(element3);
-
-    test = document.getElementById(TEST_ID);
-    assert_equals(test, element4, "should return 4th element");
-    container.removeChild(element4);
-
-
-  }, "where insertion order and tree order don't match");
-
-  test(function() {
-    var TEST_ID = "test14";
-    var a = document.createElement("a");
-    var b = document.createElement("b");
-    a.appendChild(b);
-    b.id = TEST_ID;
-    assert_equals(document.getElementById(TEST_ID), null);
-
-    gBody.appendChild(a);
-    assert_equals(document.getElementById(TEST_ID), b);
-  }, "Inserting an id by inserting its parent node");
-
-  test(function () {
-    var TEST_ID = "test15"
-    var outer = document.getElementById("outer");
-    var middle = document.getElementById("middle");
-    var inner = document.getElementById("inner");
-    outer.removeChild(middle);
-
-    var new_el = document.createElement("h1");
-    new_el.id = "heading";
-    inner.appendChild(new_el);
-    // the new element is not part of the document since
-    // "middle" element was removed previously
-    assert_equals(document.getElementById("heading"), null);
-  }, "Document.getElementById must not return nodes not present in document");
-
-  // TODO:
-  // id attribute in a namespace
-
-
-  // TODO:
-  // SVG + MathML elements with id attributes
-
-</script>
-</body>
-</html>
diff --git a/Core_DOM/tests/Node-insertBefore.html.orig b/Core_DOM/tests/Node-insertBefore.html.orig
deleted file mode 100644
index a9fc83b..0000000
--- a/Core_DOM/tests/Node-insertBefore.html.orig
+++ /dev/null
@@ -1,306 +0,0 @@
-<!DOCTYPE html>
-<title>Node.insertBefore</title>
-<script src="/resources/testharness.js"></script>
-<script src="/resources/testharnessreport.js"></script>
-<div id="log"></div>
-<script>
-function testLeafNode(nodeName, createNodeFunction) {
-  test(function() {
-    var node = createNodeFunction();
-    assert_throws(new TypeError(), function() { node.insertBefore(null, null) })
-  }, "Calling insertBefore with a non-Node first argument on a leaf node " + nodeName + " must throw TypeError.")
-  test(function() {
-    var node = createNodeFunction();
-    assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(document.createTextNode("fail"), null) })
-    // Would be step 2.
-    assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(node, null) })
-    // Would be step 3.
-    assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(node, document.createTextNode("child")) })
-  }, "Calling insertBefore an a leaf node " + nodeName + " must throw HIERARCHY_REQUEST_ERR.")
-}
-
-test(function() {
-  // WebIDL.
-  assert_throws(new TypeError(), function() { document.body.insertBefore(null, null) })
-  assert_throws(new TypeError(), function() { document.body.insertBefore(null, document.body.firstChild) })
-  assert_throws(new TypeError(), function() { document.body.insertBefore({'a':'b'}, document.body.firstChild) })
-}, "Calling insertBefore with a non-Node first argument must throw TypeError.")
-
-testLeafNode("DocumentType", function () { return document.doctype; } )
-testLeafNode("Text", function () { return document.createTextNode("Foo") })
-testLeafNode("Comment", function () { return document.createComment("Foo") })
-testLeafNode("ProcessingInstruction", function () { return document.createProcessingInstruction("foo", "bar") })
-
-test(function() {
-  // Step 2.
-  assert_throws("HIERARCHY_REQUEST_ERR", function() { document.body.insertBefore(document.body, document.getElementById("log")) })
-  assert_throws("HIERARCHY_REQUEST_ERR", function() { document.body.insertBefore(document.documentElement, document.getElementById("log")) })
-}, "Calling insertBefore with an inclusive ancestor of the context object must throw HIERARCHY_REQUEST_ERR.")
-
-// Step 3.
-test(function() {
-  var a = document.createElement("div");
-  var b = document.createElement("div");
-  var c = document.createElement("div");
-  assert_throws("NotFoundError", function() {
-    a.insertBefore(b, c);
-  });
-}, "Calling insertBefore with a reference child whose parent is not the context node must throw a NotFoundError.")
-
-// Step 4.1.
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  var doc2 = document.implementation.createHTMLDocument("title2");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doc2, doc.documentElement);
-  });
-
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doc.createTextNode("text"), doc.documentElement);
-  });
-}, "If the context node is a document, inserting a document or text node should throw a HierarchyRequestError.")
-
-// Step 4.2.1.
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  doc.removeChild(doc.documentElement);
-
-  var df = doc.createDocumentFragment();
-  df.appendChild(doc.createElement("a"));
-  df.appendChild(doc.createElement("b"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, null);
-  });
-
-  df = doc.createDocumentFragment();
-  df.appendChild(doc.createTextNode("text"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, null);
-  });
-
-  df = doc.createDocumentFragment();
-  df.appendChild(doc.createComment("comment"));
-  df.appendChild(doc.createTextNode("text"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, null);
-  });
-}, "If the context node is a document, appending a DocumentFragment that contains a text node or too many elements should throw a HierarchyRequestError.")
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  doc.removeChild(doc.documentElement);
-
-  var df = doc.createDocumentFragment();
-  df.appendChild(doc.createElement("a"));
-  df.appendChild(doc.createElement("b"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.firstChild);
-  });
-
-  df = doc.createDocumentFragment();
-  df.appendChild(doc.createTextNode("text"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.firstChild);
-  });
-
-  df = doc.createDocumentFragment();
-  df.appendChild(doc.createComment("comment"));
-  df.appendChild(doc.createTextNode("text"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.firstChild);
-  });
-}, "If the context node is a document, inserting a DocumentFragment that contains a text node or too many elements should throw a HierarchyRequestError.")
-
-// Step 4.2.2.
-test(function() {
-  // The context node has an element child.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.appendChild(doc.createComment("foo"));
-  assert_array_equals(doc.childNodes, [doc.doctype, doc.documentElement, comment]);
-
-  var df = doc.createDocumentFragment();
-  df.appendChild(doc.createElement("a"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.doctype);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.documentElement);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, comment);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, null);
-  });
-}, "If the context node is a document, inserting a DocumentFragment with an element if there already is an element child should throw a HierarchyRequestError.")
-test(function() {
-  // /child/ is a doctype.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
-  doc.removeChild(doc.documentElement);
-  assert_array_equals(doc.childNodes, [comment, doc.doctype]);
-
-  var df = doc.createDocumentFragment();
-  df.appendChild(doc.createElement("a"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, doc.doctype);
-  });
-}, "If the context node is a document and a doctype is following the reference child, inserting a DocumentFragment with an element should throw a HierarchyRequestError.")
-test(function() {
-  // /child/ is not null and a doctype is following /child/.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
-  doc.removeChild(doc.documentElement);
-  assert_array_equals(doc.childNodes, [comment, doc.doctype]);
-
-  var df = doc.createDocumentFragment();
-  df.appendChild(doc.createElement("a"));
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(df, comment);
-  });
-}, "If the context node is a document, inserting a DocumentFragment with an element before the doctype should throw a HierarchyRequestError.")
-
-// Step 4.3.
-test(function() {
-  // The context node has an element child.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.appendChild(doc.createComment("foo"));
-  assert_array_equals(doc.childNodes, [doc.doctype, doc.documentElement, comment]);
-
-  var a = doc.createElement("a");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, doc.doctype);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, doc.documentElement);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, comment);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, null);
-  });
-}, "If the context node is a document, inserting an element if there already is an element child should throw a HierarchyRequestError.")
-test(function() {
-  // /child/ is a doctype.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
-  doc.removeChild(doc.documentElement);
-  assert_array_equals(doc.childNodes, [comment, doc.doctype]);
-
-  var a = doc.createElement("a");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, doc.doctype);
-  });
-}, "If the context node is a document, inserting an element before the doctype should throw a HierarchyRequestError.")
-test(function() {
-  // /child/ is not null and a doctype is following /child/.
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
-  doc.removeChild(doc.documentElement);
-  assert_array_equals(doc.childNodes, [comment, doc.doctype]);
-
-  var a = doc.createElement("a");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(a, comment);
-  });
-}, "If the context node is a document and a doctype is following the reference child, inserting an element should throw a HierarchyRequestError.")
-
-// Step 4.4.
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
-  assert_array_equals(doc.childNodes, [comment, doc.doctype, doc.documentElement]);
-
-  var doctype = document.implementation.createDocumentType("html", "", "");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, comment);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, doc.doctype);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, doc.documentElement);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, null);
-  });
-}, "If the context node is a document, inserting a doctype if there already is a doctype child should throw a HierarchyRequestError.")
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.appendChild(doc.createComment("foo"));
-  doc.removeChild(doc.doctype);
-  assert_array_equals(doc.childNodes, [doc.documentElement, comment]);
-
-  var doctype = document.implementation.createDocumentType("html", "", "");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, comment);
-  });
-}, "If the context node is a document, inserting a doctype after the document element should throw a HierarchyRequestError.")
-test(function() {
-  var doc = document.implementation.createHTMLDocument("title");
-  var comment = doc.appendChild(doc.createComment("foo"));
-  doc.removeChild(doc.doctype);
-  assert_array_equals(doc.childNodes, [doc.documentElement, comment]);
-
-  var doctype = document.implementation.createDocumentType("html", "", "");
-  assert_throws("HierarchyRequestError", function() {
-    doc.insertBefore(doctype, null);
-  });
-}, "If the context node is a document with and element child, appending a doctype should throw a HierarchyRequestError.")
-
-// Step 5.
-test(function() {
-  var df = document.createDocumentFragment();
-  var a = df.appendChild(document.createElement("a"));
-
-  var doc = document.implementation.createHTMLDocument("title");
-  assert_throws("HierarchyRequestError", function() {
-    df.insertBefore(doc, a);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    df.insertBefore(doc, null);
-  });
-
-  var doctype = document.implementation.createDocumentType("html", "", "");
-  assert_throws("HierarchyRequestError", function() {
-    df.insertBefore(doctype, a);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    df.insertBefore(doctype, null);
-  });
-}, "If the context node is a DocumentFragment, inserting a document or a doctype should throw a HierarchyRequestError.")
-test(function() {
-  var el = document.createElement("div");
-  var a = el.appendChild(document.createElement("a"));
-
-  var doc = document.implementation.createHTMLDocument("title");
-  assert_throws("HierarchyRequestError", function() {
-    el.insertBefore(doc, a);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    el.insertBefore(doc, null);
-  });
-
-  var doctype = document.implementation.createDocumentType("html", "", "");
-  assert_throws("HierarchyRequestError", function() {
-    el.insertBefore(doctype, a);
-  });
-  assert_throws("HierarchyRequestError", function() {
-    el.insertBefore(doctype, null);
-  });
-}, "If the context node is an element, inserting a document or a doctype should throw a HierarchyRequestError.")
-
-// Step 7.
-test(function() {
-  var a = document.createElement("div");
-  var b = document.createElement("div");
-  var c = document.createElement("div");
-  a.appendChild(b);
-  a.appendChild(c);
-  assert_array_equals(a.childNodes, [b, c]);
-  assert_equals(a.insertBefore(b, b), b);
-  assert_array_equals(a.childNodes, [b, c]);
-  assert_equals(a.insertBefore(c, c), c);
-  assert_array_equals(a.childNodes, [b, c]);
-}, "Inserting a node before itself should not move the node");
-</script>
diff --git a/Core_DOM/tests/Node-removeChild.html.orig b/Core_DOM/tests/Node-removeChild.html.orig
deleted file mode 100644
index fb22583..0000000
--- a/Core_DOM/tests/Node-removeChild.html.orig
+++ /dev/null
@@ -1,54 +0,0 @@
-<!DOCTYPE html>
-<title>Node.removeChild</title>
-<script src="/resources/testharness.js"></script>
-<script src="/resources/testharnessreport.js"></script>
-<script src="creators.js"></script>
-<div id="log"></div>
-<iframe src=about:blank></iframe>
-<script>
-var documents = [
-  [function() { return document }, "the main document"],
-  [function() { return frames[0].document }, "a frame document"],
-  [function() { return document.implementation.createHTMLDocument() },
-   "a synthetic document"],
-];
-
-documents.forEach(function(d) {
-  var get = d[0], description = d[1]
-  for (var p in creators) {
-    var creator = creators[p];
-    test(function() {
-      var doc = get();
-      var s = doc[creator]("a")
-      assert_equals(s.ownerDocument, doc)
-      assert_throws("NOT_FOUND_ERR", function() { document.body.removeChild(s) })
-      assert_equals(s.ownerDocument, doc)
-    }, "Passing a detached " + p + " from " + description +
-       " to removeChild should not affect it.")
-
-    test(function() {
-      var doc = get();
-      var s = doc[creator]("b")
-      doc.documentElement.appendChild(s)
-      assert_equals(s.ownerDocument, doc)
-      assert_throws("NOT_FOUND_ERR", function() { document.body.removeChild(s) })
-      assert_equals(s.ownerDocument, doc)
-    }, "Passing a non-detached " + p + " from " + description +
-       " to removeChild should not affect it.")
-
-    test(function() {
-      var doc = get();
-      var s = doc[creator]("test")
-      doc.body.appendChild(s)
-      assert_equals(s.ownerDocument, doc)
-      assert_throws("NOT_FOUND_ERR", function() { s.removeChild(doc) })
-    }, "Calling removeChild on a " + p + " from " + description +
-       " with no children should throw NOT_FOUND_ERR.")
-  }
-});
-
-test(function() {
-  assert_throws(new TypeError(), function() { document.body.removeChild(null) })
-  assert_throws(new TypeError(), function() { document.body.removeChild({'a':'b'}) })
-}, "Passing a value that is not a Node reference to removeChild should throw TypeError.")
-</script>