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 *}