src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Thu Dec 02 21:48:36 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 03 17:59:13 2010 +0100
@@ -33,9 +33,11 @@
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
   ("Tools/type_mapper.ML")
+  "~~/src/Tools/subtyping.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
+setup Subtyping.setup
 
 
 subsection {* Primitive logic *}