changeset 45035 | 60d2c03d5c70 |
parent 42415 | 10accf397ab6 |
child 45704 | 5e547b54a9e2 |
45034:b0f61dec677a | 45035:60d2c03d5c70 |
---|---|
1 (* Title: HOL/Nitpick_Examples/Mono_Nits.thy |
1 (* Title: HOL/Nitpick_Examples/Mono_Nits.thy |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2009, 2010 |
3 Copyright 2009-2011 |
4 |
4 |
5 Examples featuring Nitpick's monotonicity check. |
5 Examples featuring Nitpick's monotonicity check. |
6 *) |
6 *) |
7 |
7 |
8 header {* Examples Featuring Nitpick's Monotonicity Check *} |
8 header {* Examples Featuring Nitpick's Monotonicity Check *} |