author | mengj |
Wed, 01 Mar 2006 06:08:12 +0100 | |
changeset 19162 | 67436e2a16df |
parent 19161 | b395f586633f |
child 19163 | b61039bf141f |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Wed Mar 01 06:06:16 2006 +0100 +++ b/src/HOL/HOL.thy Wed Mar 01 06:08:12 2006 +0100 @@ -918,6 +918,9 @@ setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *} setup Classical.setup + +setup ResAtpSet.setup + setup clasetup declare ex_ex1I [rule del, intro! 2]