| changeset 46459 | 73823dbbecc4 |
| parent 46156 | f58b7f9d3920 |
| child 46504 | cd4832aa2229 |
--- a/src/HOL/Set.thy Tue Feb 14 16:59:12 2012 +0100 +++ b/src/HOL/Set.thy Tue Feb 14 17:11:33 2012 +0100 @@ -379,7 +379,7 @@ *} declaration {* fn _ => - Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1)) + Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac)) *} ML {*