# HG changeset patch
# User wenzelm
# Date 1492767525 -7200
# Node ID 09c00a304c009e0c3c74f2f53da2232a08b1f8fb
# Parent  53fd6cf53ec2b07205122a7b878ffa89bafb08ef
include imports that morally belong to Main and are used in HOL-Proofs applications;

diff -r 53fd6cf53ec2 -r 09c00a304c00 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 21 11:21:59 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 11:38:45 2017 +0200
@@ -21,7 +21,10 @@
   options [document = false, theory_qualifier = "HOL",
     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   sessions "HOL-Library"
-  theories "HOL-Library.Old_Datatype"
+  theories
+    GCD
+    Binomial
+    "HOL-Library.Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"