--- a/src/HOL/HOL.thy Thu Sep 28 21:01:13 2006 +0200
+++ b/src/HOL/HOL.thy Thu Sep 28 23:42:30 2006 +0200
@@ -7,9 +7,7 @@
theory HOL
imports CPure
-uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
- "Tools/res_atpset.ML"
-
+uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") "Tools/res_atpset.ML"
begin
subsection {* Primitive logic *}
@@ -920,7 +918,7 @@
setup hypsubst_setup
setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
setup Classical.setup
-setup ResAtpSet.setup
+setup ResAtpset.setup
setup clasetup
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"