src/HOL/HOL.thy
changeset 41042 8275f52ac991
parent 40969 fb2d3ccda5a7
child 41184 5c6f44d22f51
--- a/src/HOL/HOL.thy	Tue Dec 07 09:58:52 2010 +0100
+++ b/src/HOL/HOL.thy	Tue Dec 07 09:58:56 2010 +0100
@@ -29,8 +29,6 @@
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
-  "Tools/async_manager.ML"
-  "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
   "~~/src/Tools/subtyping.ML"
 begin
@@ -1982,10 +1980,6 @@
 *} "solve goal by normalization"
 
 
-subsection {* Try *}
-
-setup {* Try.setup *}
-
 subsection {* Counterexample Search Units *}
 
 subsubsection {* Quickcheck *}