changeset 37781 | 2fbbf0a48cef |
parent 37767 | a2b7a20d6ea3 |
child 37877 | d4a30d210220 |
--- a/src/HOL/HOL.thy Mon Jul 12 21:12:18 2010 +0200 +++ b/src/HOL/HOL.thy Mon Jul 12 21:38:37 2010 +0200 @@ -15,6 +15,7 @@ "~~/src/Tools/intuitionistic.ML" "~~/src/Tools/project_rule.ML" "~~/src/Tools/cong_tac.ML" + "~~/src/Tools/misc_legacy.ML" "~~/src/Provers/hypsubst.ML" "~~/src/Provers/splitter.ML" "~~/src/Provers/classical.ML"