diff options
| author | Pierre Courtieu | 2014-12-16 13:07:13 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2014-12-16 13:07:13 +0000 |
| commit | c868833b20cc3c8e3962e5a18a952c84e6c47284 (patch) | |
| tree | c13dcd218090311d0776b012793ac17502177330 /isar/Example.thy | |
| parent | dbe7dde0311670da5a2bf21b253d04264a758e30 (diff) | |
Added a way to print eager message without warning face.
It is the only way I found to display informativemessage appearing
*before* the goal.
Diffstat (limited to 'isar/Example.thy')
0 files changed, 0 insertions, 0 deletions