| changeset 16121 | a80aa66d2271 |
| parent 16019 | 0e1405402d53 |
| child 16417 | 9bc16273c2d4 |
--- a/src/FOL/IFOL.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/FOL/IFOL.thy Tue May 31 11:53:12 2005 +0200 @@ -184,8 +184,8 @@ and [Pure.elim 2] = allE notE' impE' and [Pure.intro] = exI disjI2 disjI1 -ML_setup {* - Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); +setup {* + [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)] *}