equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/datatype_aux.ML |
1 (* Title: HOL/Tools/datatype_aux.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer, TU Muenchen |
4 Copyright 1998 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Auxiliary functions for defining datatypes |
6 Auxiliary functions for defining datatypes. |
7 *) |
7 *) |
8 |
8 |
9 signature DATATYPE_AUX = |
9 signature DATATYPE_AUX = |
10 sig |
10 sig |
11 val quiet_mode : bool ref |
11 val quiet_mode : bool ref |