src/HOL/ex/ROOT.ML
changeset 40281 3c6198fd0937
parent 40239 c4336e45f199
child 40349 131cf8790a1c
--- a/src/HOL/ex/ROOT.ML	Fri Oct 29 18:17:11 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Oct 29 21:34:07 2010 +0200
@@ -13,6 +13,7 @@
 
 use_thys [
   "Iff_Oracle",
+  "Coercion_Examples",
   "Numeral",
   "Higher_Order_Logic",
   "Abstract_NAT",