| changeset 54397 | f4b4fa25ce56 |
| parent 54396 | 8baee6b04a7c |
| child 54435 | 4a655e62ad34 |
| 54396:8baee6b04a7c | 54397:f4b4fa25ce56 |
|---|---|
1 (* Title: HOL/BNF/Tools/ctr_sugar_util.ML |
1 (* Title: HOL/Tools/ctr_sugar_util.ML |
2 Author: Dmitriy Traytel, TU Muenchen |
|
2 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2012 |
4 Copyright 2012, 2013 |
4 |
5 |
5 Library for wrapping existing freely generated type's constructors. |
6 Library for wrapping existing freely generated type's constructors. |
6 *) |
7 *) |
7 |
8 |
8 signature CTR_SUGAR_UTIL = |
9 signature CTR_SUGAR_UTIL = |