| changeset 46459 | 73823dbbecc4 |
| parent 46156 | f58b7f9d3920 |
| child 46504 | cd4832aa2229 |
| 46458:19ef91d7fbd4 | 46459:73823dbbecc4 |
|---|---|
377 text {* |
377 text {* |
378 Gives better instantiation for bound: |
378 Gives better instantiation for bound: |
379 *} |
379 *} |
380 |
380 |
381 declaration {* fn _ => |
381 declaration {* fn _ => |
382 Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1)) |
382 Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac)) |
383 *} |
383 *} |
384 |
384 |
385 ML {* |
385 ML {* |
386 structure Simpdata = |
386 structure Simpdata = |
387 struct |
387 struct |