changeset 39432 | 12d1be8ff862 |
parent 39421 | b6a77cffc231 |
child 39471 | 55e0ff582fa4 |
--- a/src/HOL/HOL.thy Wed Sep 15 20:07:41 2010 +0200 +++ b/src/HOL/HOL.thy Wed Sep 15 20:47:14 2010 +0200 @@ -25,7 +25,6 @@ "~~/src/Tools/eqsubst.ML" "~~/src/Provers/quantifier1.ML" ("Tools/simpdata.ML") - "~~/src/Tools/random_word.ML" "~~/src/Tools/atomize_elim.ML" "~~/src/Tools/induct.ML" ("~~/src/Tools/induct_tacs.ML")