equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar.ML |
1 (* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar.ML |
2 Author: Lorenz Panny, TU Muenchen |
2 Author: Lorenz Panny, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 Copyright 2013 |
4 Copyright 2013 |
5 |
5 |
6 Corecursor sugar. |
6 Corecursor sugar ("primcorec" and "primcorecursive"). |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_GFP_REC_SUGAR = |
9 signature BNF_GFP_REC_SUGAR = |
10 sig |
10 sig |
11 datatype primcorec_option = Sequential_Option | Exhaustive_Option |
11 datatype primcorec_option = Sequential_Option | Exhaustive_Option |