equal
deleted
inserted
replaced
916 setup hypsubst_setup |
916 setup hypsubst_setup |
917 |
917 |
918 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *} |
918 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *} |
919 |
919 |
920 setup Classical.setup |
920 setup Classical.setup |
|
921 |
|
922 setup ResAtpSet.setup |
|
923 |
921 setup clasetup |
924 setup clasetup |
922 |
925 |
923 declare ex_ex1I [rule del, intro! 2] |
926 declare ex_ex1I [rule del, intro! 2] |
924 and ex1I [intro] |
927 and ex1I [intro] |
925 |
928 |