equal
deleted
inserted
replaced
378 text {* |
378 text {* |
379 Gives better instantiation for bound: |
379 Gives better instantiation for bound: |
380 *} |
380 *} |
381 |
381 |
382 setup {* |
382 setup {* |
383 map_theory_claset (fn ctxt => ctxt addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac)) |
383 map_theory_claset (fn ctxt => |
|
384 ctxt addbefore ("bspec", fn _ => dtac @{thm bspec} THEN' assume_tac)) |
384 *} |
385 *} |
385 |
386 |
386 ML {* |
387 ML {* |
387 structure Simpdata = |
388 structure Simpdata = |
388 struct |
389 struct |