equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/BNF/bnf_lfp_util.ML |
1 (* Title: HOL/Tools/BNF/bnf_lfp_util.ML |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 Copyright 2012 |
4 Copyright 2012 |
5 |
5 |
6 Library for the datatype construction. |
6 Library for the new-style datatype construction. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_LFP_UTIL = |
9 signature BNF_LFP_UTIL = |
10 sig |
10 sig |
11 val mk_bij_betw: term -> term -> term -> term |
11 val mk_bij_betw: term -> term -> term -> term |